Ali Assaf: Embedding logics in the lambda-Pi calculus modulo rewriting
Time: Tue 2014-10-21 10.15 - 12.00
Location: Room 16, building 5, Kräftriket, Department of mathematics, Stockholm university
Participating: Ali Assaf, INRIA and École Polytechnique, Paris
The lambda-Pi calculus modulo is an extension of the lambda-Pi calculus with rewrite rules. Using the Curry-Howard correspondence, it can be used as a logical framework to define logics and express proofs in those logics in a way that preserves the reduction semantics. I will show how we embed various theories such as the calculus of constructions and simple type theory in the lambda-Pi calculus modulo rewriting and consider the soundness and completeness of these embeddings.