A Framework for Defining Type Theories

Thiago Felicissimo

Date: Wed, May 18, 2022
Time: 12:00
Room: Social Data Lab 0.E220

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 |
Next: tba |