Skip to Main content Skip to Navigation
Conference papers

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

Bruno Barras 1 Valentin Maestracci 1
1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
Inria Saclay - Ile de France, LSV - Laboratoire Spécification et Vérification
Abstract : 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 procedure in a de Morgan algebra that so far could not be expressed by the rewrite rules of Dedukti. As an alternative, 2 Layer Type Theories are variants of Martin-Lf Type Theory where all or part of the definitionalequality can be represented in terms of a so-called external equality. We propose to split the encodingby giving an encoding of 2 Layer Type Theories (2LTT) in Dedukti, and a partial encoding of CTTin 2LTT.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03138145
Contributor : Bruno Barras Connect in order to contact the contributor
Submitted on : Thursday, February 11, 2021 - 11:43:27 AM
Last modification on : Tuesday, January 4, 2022 - 6:38:27 AM
Long-term archiving on: : Wednesday, May 12, 2021 - 6:12:19 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03138145, version 1

Citation

Bruno Barras, Valentin Maestracci. Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory. LFMPT 2020 - Logical Frameworks and Meta-Languages: Theory and Practice 2020, Jun 2020, Paris, France. ⟨hal-03138145⟩

Share

Metrics

Les métriques sont temporairement indisponibles