A Framework for Defining Type Theories

Thiago Felicissimo

In this talk I’ll start by presenting the logical framework Dedukti, a language which allows for the definition of various logics and systems, and its applications for rechecking and sharing proofs. I’ll then discuss my research project, which concerns the encoding of type theories in Dedukti. One of the main practical applications of this work is the development of the Agda2Dk translator, allowing to translate Agda proofs into their representation in Dedukti.

---

Previous: Gerben Oolbekkink | Describing Inter Parameter Constraints in Web APIs Using Dependent Types
Next: | Computer formalization of Voevodsky's theory of type theories