Productive coprogramming with guarded recursion

DOI10.1145/2500365.2500597zbMath1323.68092OpenAlexW1969167499MaRDI QIDQ5244800

Robert Atkey, Conor McBride

Publication date: 30 March 2015

Published in: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL: https://strathprints.strath.ac.uk/44848/

zbMATH Keywords

coalgebrascorecursionguarded recursiontotal functional programming

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (24)

Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Lewis meets Brouwer: constructive strict implication ⋮ Doo bee doo bee doo ⋮ A model of guarded recursion via generalised equilogical spaces ⋮ The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types ⋮ A model of guarded recursion with clock synchronisation ⋮ A model of PCF in guarded type theory ⋮ Denotational semantics of recursive types in synthetic guarded domain theory ⋮ A Light Modality for Recursion ⋮ Friends with Benefits ⋮ Denotational semantics for guarded dependent type theory ⋮ Temporal refinements for guarded recursive types ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Unnamed Item ⋮ Guarded Dependent Type Theory with Coinductive Types ⋮ Unnamed Item ⋮ Modal dependent type theory and dependent right adjoints ⋮ Model Finding for Recursive Functions in SMT ⋮ Guarded cubical type theory ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Constructive Modalities with Provability Smack

Uses Software

• Coq
• Agda

This page was built for publication: Productive coprogramming with guarded recursion