4 citations · 5 across the 4 of their papers we have counts for
6 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…
Interacting Safely with an Unsafe Environment
Gilles Dowek
We give a presentation of Pure type systems where contexts need not be well-formed and show that this presentation is equivalent to the usual one. The main motivation for this pres…
Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems
Gilles Dowek
We describe the first results of a project of analyzing in which theories formal proofs can be ex- pressed. We use this analysis as the basis of interoperability between proof syst…
Free fall and cellular automata
Pablo Arrighi, Gilles Dowek
Three reasonable hypotheses lead to the thesis that physical phenomena can be described and simulated with cellular automata. In this work, we attempt to describe the motion of a p…
Non determinism through type isomorphism
Alejandro Díaz-Caro, Gilles Dowek
We define an equivalence relation on propositions and a proof system where equivalent propositions have the same proofs. The system obtained this way resembles several known non-de…
The physical Church-Turing thesis and the principles of quantum theory
Pablo Arrighi, Gilles Dowek
Notoriously, quantum computation shatters complexity theory, but is innocuous to computability theory. Yet several works have shown how quantum theory as it stands could breach the…