References & Citations
Computer Science > Programming Languages
Title: Programming and Reasoning with Guarded Recursion for Coinductive Types
(Submitted on 13 Jan 2015 (v1), last revised 15 Jan 2015 (this version, v2))
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.
Submission history
From: Ranald Clouston [view email][v1] Tue, 13 Jan 2015 09:24:28 GMT (57kb)
[v2] Thu, 15 Jan 2015 12:37:21 GMT (57kb)
Link back to: arXiv, form interface, contact.