A stratified approach to Löb induction

DOI10.4230/LIPICS.FSCD.2022.23MaRDI QIDQ6544118zbMATH OpenFDO

Authors Daniel Gratzer, Lars Birkedal

Publication date 27 May 2024

Full work available at URL https://doi.org/10.4230/LIPICS.FSCD.2022.23

zbMATH Keywords

canonicitycategorical gluingdependent type theoryguarded recursionmodal type theory

Mathematics Subject Classification ID

Type theory (03B38) Modal logic (including the logic of norms) (03B45)

Recommendations

• Guarded dependent type theory with coinductive types
• Guarded cubical type theory
• Guarded cubical type theory: path equality for guarded recursion
• Denotational semantics for guarded dependent type theory
• The clocks are ticking: no more delays!: Reduction semantics for type theory with guarded recursion

Cited in

(2)

• Normalization for multimodal type theory
• Strict universes for Grothendieck topoi

This page was built for publication: A stratified approach to Löb induction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6544118)