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

Abstract

We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive types may be transformed into coinductive types by a type-former inspired by modal logic and Atkey-McBride clock quantification, allowing the typing of acausal functions. We give a call-by-name operational semantics for the calculus, and define adequate denotational semantics in the topos of trees. The adequacy proof entails that the evaluation of a program always terminates. We introduce a program logic with Löb induction for reasoning about the contextual equivalence of programs. We demonstrate the expressiveness of the calculus by showing the definability of solutions to Rutten's behavioural differential equations.

Accepted to Logical Methods in Computer Science special issue on the 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015)

References in corpus (1)

• Constructive Modalities with Provability Smack

Cited by in corpus (7)

• A Generalized Modality for Recursion
• Dual-Context Calculi for Modal Logic
• Modalities, Cohesion, and Information Flow
• A Metalanguage for Guarded Iteration
• Sikkel: Multimode Simple Type Theory as an Agda Library
• A Totally Predictable Outcome: An Investigation of Traversals of Infinite Structures
• Deriving Dependently-Typed OOP from First Principles -- Extended Version with Additional Appendices