Clouston, Ranald and Bizjak, Aleš and Grathwohl, Hans Bugge and Birkedal, Lars - The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types

lmcs:2019 - Logical Methods in Computer Science, September 6, 2016, Volume 12, Issue 3
The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types

Authors: Clouston, Ranald and Bizjak, Aleš and Grathwohl, Hans Bugge and Birkedal, Lars

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.


Source : oai:arXiv.org:1606.09455
DOI : 10.2168/LMCS-12(3:7)2016
Volume: Volume 12, Issue 3
Published on: September 6, 2016
Submitted on: September 6, 2016
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages


Share

Browsing statistics

This page has been seen 324 times.
This article's PDF has been downloaded 49 times.