collaborators

1 paper

cs.LO2021

Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory

Bruno Barras, Valentin Maestracci

In this paper, we make a substantial step towards an encoding of Cubical Type Theory (CTT) in the Dedukti logical framework. Type-checking CTT expressions features a decision proce…