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

lmcs:2019 - Logical Methods in Computer Science, April 27, 2017, Volume 12, Issue 3 - https://doi.org/10.2168/LMCS-12(3:7)2016
The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive TypesArticle

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

    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.


    Volume: Volume 12, Issue 3
    Published on: April 27, 2017
    Accepted on: September 6, 2016
    Submitted on: November 27, 2015
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages

    10 Documents citing this article

    Consultation statistics

    This page has been seen 2997 times.
    This article's PDF has been downloaded 574 times.