Cover Image

Kuroda's Translation for the $λΠ$-Calculus Modulo Theory and Dedukti

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Traversié, Thomas
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Proofs for Free in the $λΠ$-Calculus Modulo Theory
by: Traversié, Thomas
Published: (2024)

From Rewrite Rules to Axioms in the $λ$$Π$-Calculus Modulo Theory
by: Blot, Valentin, et al.
Published: (2024)

Kuroda's Translation for Higher-Order Logic
by: Traversié, Thomas
Published: (2024)

Formalizing Representation Theorems for a Logical Framework with Rewriting
by: Traversié, Thomas, et al.
Published: (2025)

A Classical Linear $λ$-Calculus based on Contraposition
by: Barenbaum, Pablo, et al.
Published: (2026)

Fully Abstract Encodings of $λ$-Calculus in HOcore through Abstract Machines
by: Biernacka, Małgorzata, et al.
Published: (2022)

Reasonable Space for the $λ$-Calculus, Logarithmically
by: Accattoli, Beniamino, et al.
Published: (2022)

Generalized Optimization Modulo Theories
by: Tsiskaridze, Nestan, et al.
Published: (2024)

Unification with Simple Variable Restrictions and Admissibility of $Π_{2}$-rules
by: Almeida, Rodrigo Nicolau, et al.
Published: (2024)

$Π_{2}$-Rule Systems and Inductive Classes of Gödel Algebras
by: Almeida, Rodrigo Nicolau
Published: (2023)

Satisfiability Modulo Theories for Verifying MILP Certificates
by: Wood, Kenan, et al.
Published: (2023)

DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories
by: Feng, Nick, et al.
Published: (2024)

$Π_{2}^{P}$ vs PSpace Dichotomy for the Quantified Constraint Satisfaction Problem
by: Zhuk, Dmitriy
Published: (2024)

A Rewriting Theory for Quantum Lambda-Calculus
by: Faggian, Claudia, et al.
Published: (2024)

Canonical Decision Diagrams Modulo Theories
by: Michelutti, Massimo, et al.
Published: (2024)

Complete and Terminating Tableau Calculus for Undirected Graph
by: Nishimura, Yuki, et al.
Published: (2024)

A Unified Automata-Theoretic Approach to LTLf Modulo Theories (Extended Version)
by: Faella, Marco, et al.
Published: (2024)

Heterogeneous Dynamic Logic: Provability Modulo Program Theories
by: Teuber, Samuel, et al.
Published: (2025)

The Flower Calculus
by: Donato, Pablo
Published: (2024)

MCSAT Modulo Transcendental Arithmetics
by: Gallego-Hernández, Jorge, et al.
Published: (2026)

Congruence Closure Modulo Groups
by: Kim, Dohan
Published: (2023)

Note on a Translation from First-Order Logic into the Calculus of Relations Preserving Validity and Finite Validity
by: Nakamura, Yoshiki
Published: (2023)

Variable Elimination as Rewriting in a Linear Lambda Calculus
by: Ehrhard, Thomas, et al.
Published: (2025)

A Translation of Probabilistic Event Calculus into Markov Decision Processes
by: Xu, Lyris, et al.
Published: (2025)

Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search
by: Lipparini, Enrico, et al.
Published: (2025)

A Cut-free Sequent Calculus for Basic Intuitionistic Dynamic Topological Logic
by: Tabatabai, Amirhossein Akbar, et al.
Published: (2025)

Satisfiability Modulo Exponential Integer Arithmetic
by: Frohn, Florian, et al.
Published: (2024)

The Tensor-Plus Calculus
by: Chardonnet, Kostia, et al.
Published: (2025)

Neuro-Symbolic Constrained Optimization for Cloud Application Deployment via Graph Neural Networks and Satisfiability Modulo Theory
by: Erascu, Madalina
Published: (2025)

On the complexity of normalization for the planar $λ$-calculus
by: Das, Anupam, et al.
Published: (2024)

The $K_\infty$ Homotopy $λ$-Model
by: Martínez-Rivillas, Daniel O., et al.
Published: (2025)

Exploiting Partial-Assignment Enumeration in Optimization Modulo Theories
by: Masina, Gabriele, et al.
Published: (2025)

Optimization Modulo Integer Linear-Exponential Programs
by: Hitarth, S, et al.
Published: (2025)

Integer Reasoning Modulo Different Constants in SMT
by: Pertseva, Elizaveta, et al.
Published: (2025)

Applications of Interval-based Temporal Separation: the Reactivity Normal Form, Inverse $Π$, Craig Interpolation and Beth Definability
by: Guelev, Dimitar P.
Published: (2025)

Modulo quantifiers over functional vocabularies extending addition
by: Baskar, A., et al.
Published: (2017)

Satisfiability Modulo Extensional Constant Arrays (Extended Version)
by: Preiner, Mathias, et al.
Published: (2026)

An Effective Orchestral Approach to Satisfiability Modulo Prime Fields
by: Isabel, Miguel, et al.
Published: (2026)

Proofs as Execution Trees for the π-Calculus
by: Acclavio, Matteo, et al.
Published: (2024)

Groups and Inverse Semigroups in Lambda Calculus
by: Bucciarelli, Antonio, et al.
Published: (2026)