research
∙
09/21/2023
The Undecidability of Third Order Pattern Matching in Calculi with Dependent Types or Type Constructors
We prove the undecidability of the third order pattern matching problem ...
share
research
∙
09/07/2023
On Statman's Finite Completeness Theorem
We give a complete self-contained proof of Statman's finite completeness...
research
∙
09/05/2023
A Unification Algorithm for Second-Order Linear Terms
We give an algorithm for the class of second order unification problems ...
research
∙
07/03/2023
On the Definition of the Eta-long Normal Form in Type Systems of the Cube
The smallest transitive relation < on well-typed normal terms such that ...
research
∙
06/13/2023
The Undecidability of Typability in the Lambda-Pi-Calculus
The set of pure terms which are typable in the λΠ-calculus in a given co...
research
∙
06/12/2023
A toy model provably featuring an arrow of time without past hypothesis
The laws of Physics are time-reversible, making no qualitative distincti...
research
∙
06/09/2023
The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable
We prove that the pattern matching problem is undecidable in polymorphic...
research
∙
06/09/2023
A Complete Proof Synthesis Method for the Cube of Type Systems
We present a complete proof synthesis method for the eight type systems ...
research
∙
06/02/2023
Third Order Matching is Decidable
The higher order matching problem is the problem of determining whether ...
research
∙
06/01/2023
Automated theorem proving in first-order logic modulo: on the difference between type theory and set theory
Resolution modulo is a first-order theorem proving method that can be ap...
research
∙
06/01/2023
Axioms vs. rewrite rules: from completeness to cut elimination
Combining a standard proof search method, such as resolution or tableaux...
research
∙
06/01/2023
From proof theory to theories theory
In the last decades, several objects such as grammars, economical agents...
research
∙
05/30/2023
The Stratified Foundations as a theory modulo
The Stratified Foundations are a restriction of naive set theory where t...
research
∙
05/25/2023
Binding Logic: proofs and models
We define an extension of predicate logic, called Binding Logic, where v...
research
∙
05/25/2023
What is a Theory ?
Deduction modulo is a way to express a theory using computation rules in...
research
∙
05/24/2023
Preliminary investigations on induction over real numbers
The induction principle for natural numbers expresses that when a proper...
research
∙
05/23/2023
Confluence as a cut elimination property
The goal of this note is to compare two notions, one coming from the the...
research
∙
05/17/2023
A constructive proof of Skolem theorem for constructive logic
If the sequent (Gamma entails forall x exists y A) is provable in first ...
research
∙
05/17/2023
What do we know when we know that a theory is consistent?
Given a first-order theory and a proof that it is consistent, can we des...
research
∙
05/15/2023
Eigenvariables, bracketing and the decidability of positive minimal predicate logic
We give a new proof of a theorem of Mints that the positive fragment of ...
research
∙
05/12/2023
Truth values algebras and proof normalization
We extend the notion of Heyting algebra to a notion of truth values alge...
research
∙
05/09/2023
The Undecidability of Unification Modulo σ Alone
The rewriting system sigma is the set of rules propagating explicit subs...
research
∙
05/05/2023
Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View
Peter Andrews has proposed, in 1971, the problem of finding an analog of...
research
∙
05/02/2023
Enumerating proofs of positive formulae
We provide a semi-grammatical description of the set of normal proofs of...
research
∙
05/02/2023
On the convergence of reduction-based and model-based methods in proof theory
In the recent past, the reduction-based and the model-based methods to p...
research
∙
04/26/2023
Specifying programs with propositions and with congruences
We give a presentation of Krivine and Parigot's Second-order functional ...
research
∙
04/26/2023
Simple Type Theory as a Clausal Theory
We give a presentation of Simple Type Theory as a clausal rewrite system...
research
∙
04/26/2023
The physical Church thesis and the sensitivity to initial conditions
The physical Church thesis is a thesis about nature that expresses that ...
research
∙
04/24/2023
On the Expressive Power of Schemes
We present a calculus, called the scheme-calculus, that permits to expre...
research
∙
04/24/2023
How can we prove that a proof search method is not an instance of another?
We introduce a method to prove that a proof search method is not an inst...
research
∙
04/21/2023
A Simple Proof That Super-Consistency Implies Cut Elimination
We give a simple and direct proof that super-consistency implies the cut...
research
∙
04/19/2023
The physical Church-Turing thesis and non deterministic computation over the real numbers
On the real numbers, the notions of a semi-decidable relation and that o...
research
∙
04/17/2023
A theory independent Curry-De Bruijn-Howard correspondence
Instead of developing a customized typed lambda-calculus for each theory...
research
∙
04/17/2023
The principle of a finite density of information
The possibility to describe the laws of the Universe in a computational ...
research
∙
04/11/2023
Complementation: a bridge between finite and infinite proofs
When a proposition has no proof in an inference system, it is sometimes ...
research
∙
04/11/2023
Execution traces and reduction sequences
In this note, we defend that the notion of algorithm as a set of executi...
research
∙
04/06/2023
Logipedia: a multi-system encyclopedia of formal proofs
Libraries of formal proofs are an important part of our mathematical her...
research
∙
04/03/2023
Explanation: from ethics to logic
When a decision, such as the approval or denial of a bank loan, is deleg...
research
∙
03/31/2023
Teaching Gödel's incompleteness theorems
The basic notions of logic-predicate logic, Peano arithmetic, incomplete...
research
∙
01/26/2022
Linear lambda-calculus is linear
We prove a linearity theorem for an extension of linear logic with addit...
research
∙
10/31/2021
Some axioms for mathematics
The lambda-Pi-calculus modulo theory is a logical framework in which man...
research
∙
07/16/2021
Interacting Safely with an Unsafe Environment
We give a presentation of Pure type systems where contexts need not be w...
research
∙
12/16/2020
A New Connective in Natural Deduction, and its Application to Quantum Computing
We investigate an unsuspected connection between non harmonious logical ...
research
∙
02/10/2020
Extensional proofs in a propositional logic modulo isomorphisms
System I is a proof language for a fragment of propositional logic where...
research
∙
12/05/2017