Guarded recursion in Agda via sized types

DOI10.4230/LIPICS.FSCD.2019.32MaRDI QIDQ5089035zbMATH OpenFDO

Authors Niccolò Veltri, Niels van der Weide

Publication date 18 July 2022

zbMATH Keywords

semanticstype theorycoinductionguarded recursionsized types

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx)

Recommendations

• Programming and reasoning with guarded recursion for coinductive types
• A type theory for productive coprogramming via guarded recursion
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• The clocks are ticking: no more delays!: Reduction semantics for type theory with guarded recursion
• Guarded dependent type theory with coinductive types

Cites work

• scientific article; zbMATH DE number 7362470 (Why is no real title available?)
• A formalized proof of strong normalization for guarded recursive types
• A type theory for productive coprogramming via guarded recursion
• Copatterns, programming infinite structures by observations
• Explicit substitutions
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Guarded dependent type theory with coinductive types
• Infinite objects in type theory
• Productive coprogramming with guarded recursion
• Programming and reasoning with guarded recursion for coinductive types
• Sheaves in geometry and logic: a first introduction to topos theory
• Subtyping, declaratively. An exercise in mixed induction and coinduction
• The clocks are ticking: no more delays!: Reduction semantics for type theory with guarded recursion
• The clocks they are adjunctions. Denotational semantics for clocked type theory
• Type theory in type theory using quotient inductive types
• Type theory should eat itself
• Type-Based Productivity of Stream Definitions in the Calculus of Constructions

Cited in

(8)

• scientific article; zbMATH DE number 7779294 (Why is no real title available?)
• Temporal refinements for guarded recursive types
• Streams of approximations, equivalence of recursive effectful programs
• Formal definitions and proofs for partial (co)recursive functions
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Greatest HITs: higher inductive types in coinductive definitions via induction under clocks
• Denotational semantics for guarded dependent type theory
• Is sized typing for Coq practical?

This page was built for publication: Guarded recursion in Agda via sized types

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