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

TL;DR

The paper introduces the guarded lambda-calculus, an extension with guarded recursive and coinductive types, ensuring productivity and enabling reasoning about acausal functions with a new logic and semantics.

Contribution

It presents a novel guarded lambda-calculus with a type-former inspired by modal logic, along with operational and denotational semantics, and a logic for reasoning about program equivalence.

Findings

Ensures productivity of well-typed programs through guarded recursive types

Provides a call-by-name operational semantics and a topos of trees denotational semantics

Demonstrates expressiveness by solving Rutten's behavioral differential equations

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\"ob 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.