A Modal Deconstruction of Löb Induction

Daniel Gratzer

doi:10.1145/3704866

A Modal Deconstruction of Löb Induction

Daniel Gratzer^*

^*Corresponding author for this work

Department of Computer Science

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaper › Journal article › Research › peer-review

Abstract

We present a novel analysis of the fundamental Löb induction principle from guarded recursion. Taking advantage of recent work in modal type theory and univalent foundations, we derive Löb induction from a simpler and more conceptual set of primitives. We then capitalize on these insights to present Gatsby, the first guarded type theory capturing the rich modal structure of the topos of trees alongside Löb induction without immediately precluding canonicity or normalization. We show that Gatsby can recover many prior approaches to guarded recursion and use its additional power to improve on prior examples. We crucially rely on homotopical insights and Gatsby constitutes a new application of univalent foundations to the theory of programming languages.

Original language	English
Article number	30
Journal	Proceedings of the ACM on Programming Languages
Volume	9
ISSN	2475-1421
DOIs	https://doi.org/10.1145/3704866
Publication status	Published - 7 Jan 2025

Keywords

cubical type theory
Guarded recursion
homotopy type theory
modal type theory

Access to Document

10.1145/3704866

Library access?

Check availability with the Royal Danish Library

Cite this

@article{26729ed2b34a48e0a0dd0d716aeed74b,

title = "A Modal Deconstruction of L{\"o}b Induction",

abstract = "We present a novel analysis of the fundamental L{\"o}b induction principle from guarded recursion. Taking advantage of recent work in modal type theory and univalent foundations, we derive L{\"o}b induction from a simpler and more conceptual set of primitives. We then capitalize on these insights to present Gatsby, the first guarded type theory capturing the rich modal structure of the topos of trees alongside L{\"o}b induction without immediately precluding canonicity or normalization. We show that Gatsby can recover many prior approaches to guarded recursion and use its additional power to improve on prior examples. We crucially rely on homotopical insights and Gatsby constitutes a new application of univalent foundations to the theory of programming languages.",

keywords = "cubical type theory, Guarded recursion, homotopy type theory, modal type theory",

author = "Daniel Gratzer",

note = "Publisher Copyright: {\textcopyright} 2025 Copyright held by the owner/author(s).",

year = "2025",

month = jan,

day = "7",

doi = "10.1145/3704866",

language = "English",

volume = "9",

journal = "Proceedings of the ACM on Programming Languages ",

issn = "2475-1421",

publisher = "Association for Computing Machinery",

}

TY - JOUR

T1 - A Modal Deconstruction of Löb Induction

AU - Gratzer, Daniel

PY - 2025/1/7

Y1 - 2025/1/7

N2 - We present a novel analysis of the fundamental Löb induction principle from guarded recursion. Taking advantage of recent work in modal type theory and univalent foundations, we derive Löb induction from a simpler and more conceptual set of primitives. We then capitalize on these insights to present Gatsby, the first guarded type theory capturing the rich modal structure of the topos of trees alongside Löb induction without immediately precluding canonicity or normalization. We show that Gatsby can recover many prior approaches to guarded recursion and use its additional power to improve on prior examples. We crucially rely on homotopical insights and Gatsby constitutes a new application of univalent foundations to the theory of programming languages.

AB - We present a novel analysis of the fundamental Löb induction principle from guarded recursion. Taking advantage of recent work in modal type theory and univalent foundations, we derive Löb induction from a simpler and more conceptual set of primitives. We then capitalize on these insights to present Gatsby, the first guarded type theory capturing the rich modal structure of the topos of trees alongside Löb induction without immediately precluding canonicity or normalization. We show that Gatsby can recover many prior approaches to guarded recursion and use its additional power to improve on prior examples. We crucially rely on homotopical insights and Gatsby constitutes a new application of univalent foundations to the theory of programming languages.

KW - cubical type theory

KW - Guarded recursion

KW - homotopy type theory

KW - modal type theory

UR - https://www.scopus.com/pages/publications/85215846912

U2 - 10.1145/3704866

DO - 10.1145/3704866

M3 - Journal article

AN - SCOPUS:85215846912

SN - 2475-1421

VL - 9

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

M1 - 30

ER -

A Modal Deconstruction of Löb Induction

Abstract

Keywords

Access to Document

Library access?

Other files and links

Fingerprint

Cite this