Ali Assaf: Embedding logics in the lambda-Pi calculus modulo rewriting

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.