Embedding Pure Type Systems in the lambda-Pi-calculus modulo

Denis Cousineau, Gilles Dowek

The lambda-Pi-calculus allows to express proofs of minimal predicate logic. It can be extended, in a very simple way, by adding computation rules. This leads to the lambda-Pi-calcu…