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

Autor: Clouston, Ranald, Bizjak, Aleš, Grathwohl, Hans Bugge, Birkedal, Lars
Rok vydání: 2016
Předmět:
Zdroj: Logical Methods in Computer Science, Volume 12, Issue 3 (April 27, 2017) lmcs:2019
Druh dokumentu: Working Paper
DOI: 10.2168/LMCS-12(3:7)2016
Popis: 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.
Comment: Accepted to Logical Methods in Computer Science special issue on the 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015)
Databáze: arXiv