The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types

DOI10.2168/LMCS-12(3:7)2016zbMath1445.03012arXiv1606.09455OpenAlexW2462468993MaRDI QIDQ2974778

Ranald Clouston, Hans Bugge Grathwohl, Aleš Bizjak, Lars Birkedal

Publication date: 11 April 2017

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

Full work available at URL: https://arxiv.org/abs/1606.09455

zbMATH Keywords

denotational semanticstyped lambda-calculusprogram logicguarded recursioncoinductive types

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items (8)

Unnamed Item ⋮ Unnamed Item ⋮ Denotational semantics for guarded dependent type theory ⋮ Temporal refinements for guarded recursive types ⋮ A metalanguage for guarded iteration ⋮ Unnamed Item ⋮ Guarded cubical type theory ⋮ Unnamed Item

Uses Software

• Unnamed Item
• ModuRes
• MiniAgda
• cubicaltt
• MiniML

Cites Work

• Unnamed Item
• The category-theoretic solution of recursive metric-space equations
• Sheaves in geometry and logic: a first introduction to topos theory
• On an intuitionistic modal logic
• Behavioural differential equations: a coinductive calculus of streams, automata, and power series
• A Formalized Proof of Strong Normalization for Guarded Recursive Types
• Guarded Dependent Type Theory with Coinductive Types
• Abstract GSOS Rules and a Modular Treatment of Recursive Definitions
• Higher-order functional reactive programming in bounded space
• ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages
• Sequent Calculus in the Topos of Trees
• Programming and Reasoning with Guarded Recursion for Coinductive Types
• Higher-order ghost state
• Extending Type Theory with Forcing
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming
• A very modal model of a modern, major, general type system
• A modal analysis of staged computation
• Subtyping, Declaratively
• A type theory for productive coprogramming via guarded recursion
• Mix-Automatic Sequences
• Pure type systems with corecursion on streams
• A Model of Countable Nondeterminism in Guarded Type Theory
• A semantic model for graphical user interfaces
• Productive coprogramming with guarded recursion
• Higher-order functional reactive programming without spacetime leaks
• Constructive Modalities with Provability Smack
• Circular Coinduction in Coq Using Bisimulation-Up-To Techniques
• Impredicative Concurrent Abstract Predicates
• Applicative programming with effects
• A model of guarded recursion with clock synchronisation

This page was built for publication: The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types