Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review
Final published version
Guarded type theory extends type theory with a handful of modalities and constants to encode productive recursion. While these theories have seen widespread use, the metatheory of guarded type theories, particularly guarded dependent type theories remains underdeveloped. We show that integrating Löb induction is the key obstruction to unifying guarded recursion and dependence in a well-behaved type theory and prove a no-go theorem sharply bounding such type theories. Based on these results, we introduce GuTT: a stratified guarded type theory. GuTT is properly two type theories, sGuTT and dGuTT. The former contains only propositional rules governing Löb induction but enjoys decidable type-checking while the latter extends the former with definitional equalities. Accordingly, dGuTT does not have decidable type-checking. We prove, however, a novel guarded canonicity theorem for dGuTT, showing that programs in dGuTT can be run. These two type theories work in concert, with users writing programs in sGuTT and running them in dGuTT.
Original language | English |
---|---|
Title of host publication | 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022 |
Editors | Amy P. Felty |
Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
Publication year | Jun 2022 |
Article number | 23 |
ISBN (Electronic) | 9783959772334 |
DOIs | |
Publication status | Published - Jun 2022 |
Event | 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022 - Haifa, Israel Duration: 2 Aug 2022 → 5 Aug 2022 |
Conference | 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022 |
---|---|
Land | Israel |
By | Haifa |
Periode | 02/08/2022 → 05/08/2022 |
Series | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
Volume | 228 |
ISSN | 1868-8969 |
Publisher Copyright:
© Daniel Gratzer and Lars Birkedal
See relations at Aarhus University Citationformats
ID: 278732015