Back to Search
Start Over
Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory
- Source :
- LFMPT 2020-Logical Frameworks and Meta-Languages: Theory and Practice 2020, LFMPT 2020-Logical Frameworks and Meta-Languages: Theory and Practice 2020, Jun 2020, Paris, France
- Publication Year :
- 2021
-
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-L\"of Type Theory where all or part of the definitional equality can be represented in terms of a so-called external equality. We propose to split the encoding by giving an encoding of 2 Layer Type Theories (2LTT) in Dedukti, and a partial encoding of CTT in 2LTT.<br />Comment: In Proceedings LFMTP 2020, arXiv:2101.02835
- Subjects :
- FOS: Computer and information sciences
Computer Science - Logic in Computer Science
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
020207 software engineering
02 engineering and technology
Type (model theory)
16. Peace & justice
Logic in Computer Science (cs.LO)
Algebra
Logical framework
Type theory
0202 electrical engineering, electronic engineering, information engineering
Encoding (semiotics)
020201 artificial intelligence & image processing
Layer (object-oriented design)
De Morgan algebra
Mathematics
Subjects
Details
- Language :
- English
- Database :
- OpenAIRE
- Journal :
- LFMPT 2020-Logical Frameworks and Meta-Languages: Theory and Practice 2020, LFMPT 2020-Logical Frameworks and Meta-Languages: Theory and Practice 2020, Jun 2020, Paris, France
- Accession number :
- edsair.doi.dedup.....615c50709bb6550c1d8283cd69acee49