Programming and Reasoning with Guarded Recursion for Coinductive Types

TL;DR

This paper introduces the guarded lambda-calculus, an extension with guarded recursive and coinductive types that guarantees productivity and enables reasoning about acausal functions and behavioral differential equations.

Contribution

It presents a new calculus with guarded recursion, provides operational and denotational semantics, and develops a logic for reasoning about program equivalence.

Findings

Guarded recursive types ensure program productivity.

The calculus can define solutions to behavioral differential equations.

A program logic with L"{o}b induction is developed for reasoning.

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 demonstrate the expressiveness of the calculus by showing the definability of solutions to Rutten's behavioural differential equations. We introduce a program logic with L\"{o}b induction for reasoning about the contextual equivalence of programs.