natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Guarded recursion is a form of recursion that ensures that solutions of self-referential descriptions exist. This is achieved by “guarding” the recursive occurrence of the object under consideration using a unary modality $\blacktriangleright$ and pronounced “later”.
The later modality was first considered by Nakano (Nakano 2000) and used to ensure productivity of coinductively defined programs.
For example, for an object $A$, the type of guarded streams is the unique solution to the equation
The intended meaning is that the head of the stream is available now while the tail is only available after one step of computation.
(There are other forms of guarded recursion which act through syntactic restriction.)
Robert Atkey, Conor McBride, Productive Coprogramming with Guarded Recursion, (Productive Coprogramming with Guarded Recursion)
Aleš Bizjak, On Semantics and Applications of Guarded Recursion, (PhD thesis)
Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, Lars Birkedal, The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types, (arXiv:1606.09455)
Nakano Hiroshi, 2000, A Modality for Recursion. In Logic in Computer Science (LICS’00). (pdf)
Lars Birkedal, Ales Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, Andrea Vezzosi, Guarded cubical type theory arxiv
Jon Sterling, Robert Harper, Guarded Computational Type Theory, LICS ‘18 (2018) 879–888 [arxiv:1804.09098, doi:10.1145/3209108.3209153]
A general calculus for dependent modal type theories.
Last revised on February 14, 2023 at 11:42:48. See the history of this page for a list of all contributions to it.