3 citations · 4 across the 3 of their papers we have counts for
11 papers
The Undecidability of Typability in the Lambda-Pi-Calculus
Gilles Dowek
The set of pure terms which are typable in the -calculus in a given context is not recursive. So there is no general type inference algorithm for the programming language Elf…
The Undecidability of Pattern Matching in Calculi where Primitive Recursive Functions are Representable
Gilles Dowek
We prove that the pattern matching problem is undecidable in polymorphic lambda-calculi (as Girard's system F) and calculi supporting inductive types (as G{ö}del's system T) by red…
A Complete Proof Synthesis Method for the Cube of Type Systems
Gilles Dowek
We present a complete proof synthesis method for the eight type systems of Barendregt's cube extended with -conversion. Because these systems verify the proofs-as-objects paradi…
Third Order Matching is Decidable
Gilles Dowek
The higher order matching problem is the problem of determining whether a term is an instance of another in the simply typed -calculus, i.e. to solve the equation a = b where a…
Automated theorem proving in first-order logic modulo: on the difference between type theory and set theory
Gilles Dowek
Resolution modulo is a first-order theorem proving method that can be applied both to first-order presentations of simple type theory (also called higher-order logic) and to set th…
Axioms vs. rewrite rules: from completeness to cut elimination
Gilles Dowek
Combining a standard proof search method, such as resolution or tableaux, and rewriting is a powerful way to cut off search space in automated theorem proving, but proving the comp…