General Recursion via Coinductive Types

DOI10.2168/LMCS-1(2:1)2005zbMath1125.68038MaRDI QIDQ5310638

Venanzio Capretta

Publication date: 11 October 2007

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Mathematics Subject Classification ID

Recursive functions and relations, subrecursive hierarchies (03D20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (26)

Monads for behaviour ⋮ Soundness Conditions for Big-Step Semantics ⋮ The coinductive resumption monad ⋮ The Scott model of PCF in univalent type theory ⋮ Partiality and Container Monads ⋮ Implementing Cantor’s Paradise ⋮ Some Domain Theory and Denotational Semantics in Coq ⋮ Trace-Based Coinductive Operational Semantics for While ⋮ Quotienting the delay monad by weak bisimilarity ⋮ Unnamed Item ⋮ Turing-Completeness Totally Free ⋮ A coinductive calculus for asynchronous side-effecting processes ⋮ Streams of approximations, equivalence of recursive effectful programs ⋮ Coalgebras in functional programming and type theory ⋮ A model of PCF in guarded type theory ⋮ Denotational semantics of recursive types in synthetic guarded domain theory ⋮ Unifying Guarded and Unguarded Iteration ⋮ Partiality, Revisited ⋮ A Type of Partial Recursive Functions ⋮ Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot ⋮ Partiality, State and Dependent Types ⋮ Complete Elgot monads and coalgebraic resumptions ⋮ Unnamed Item ⋮ Another Look at Function Domains ⋮ A Coinductive Calculus for Asynchronous Side-Effecting Processes ⋮ Inductive and Coinductive Components of Corecursive Functions in Coq

This page was built for publication: General Recursion via Coinductive Types