Aarhus University Seal

A Stratified Approach to Löb Induction

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

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 languageEnglish
Title of host publication7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022
EditorsAmy P. Felty
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Publication yearJun 2022
Article number23
ISBN (Electronic)9783959772334
DOIs
Publication statusPublished - Jun 2022
Event7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022 - Haifa, Israel
Duration: 2 Aug 20225 Aug 2022

Conference

Conference7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022
LandIsrael
ByHaifa
Periode02/08/202205/08/2022
SeriesLeibniz International Proceedings in Informatics, LIPIcs
Volume228
ISSN1868-8969

Bibliographical note

Publisher Copyright:
© Daniel Gratzer and Lars Birkedal

    Research areas

  • canonicity, categorical gluing, Dependent type theory, guarded recursion, modal type theory

See relations at Aarhus University Citationformats

ID: 278732015