Guarded recursion in Agda via sized types

DOI10.4230/LIPICS.FSCD.2019.32MaRDI QIDQ5089035FDOQ5089035

Authors: Niccolò Veltri, Niels van der Weide 

Publication date: 18 July 2022

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

zbMATH Keywords

semanticstype theorycoinductionguarded recursionsized types

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (8)

• Title not available (Why is that?)
• 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)