The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
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-forme...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2017-04-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/2019/pdf |
| _version_ | 1797268607863881728 |
|---|---|
| author | Ranald Clouston Aleš Bizjak Hans Bugge Grathwohl Lars Birkedal |
| author_facet | Ranald Clouston Aleš Bizjak Hans Bugge Grathwohl Lars Birkedal |
| author_sort | Ranald Clouston |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:35:10Z |
| format | Article |
| id | doaj.art-1366e42ab74d4ccda101393e79dfd4de |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:35:10Z |
| publishDate | 2017-04-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-1366e42ab74d4ccda101393e79dfd4de2024-03-08T09:44:45ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742017-04-01Volume 12, Issue 310.2168/LMCS-12(3:7)20162019The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive TypesRanald CloustonAleš BizjakHans Bugge GrathwohlLars BirkedalWe 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.https://lmcs.episciences.org/2019/pdfcomputer science - logic in computer sciencecomputer science - programming languages |
| spellingShingle | Ranald Clouston Aleš Bizjak Hans Bugge Grathwohl Lars Birkedal The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types Logical Methods in Computer Science computer science - logic in computer science computer science - programming languages |
| title | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types |
| title_full | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types |
| title_fullStr | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types |
| title_full_unstemmed | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types |
| title_short | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types |
| title_sort | guarded lambda calculus programming and reasoning with guarded recursion for coinductive types |
| topic | computer science - logic in computer science computer science - programming languages |
| url | https://lmcs.episciences.org/2019/pdf |
| work_keys_str_mv | AT ranaldclouston theguardedlambdacalculusprogrammingandreasoningwithguardedrecursionforcoinductivetypes AT alesbizjak theguardedlambdacalculusprogrammingandreasoningwithguardedrecursionforcoinductivetypes AT hansbuggegrathwohl theguardedlambdacalculusprogrammingandreasoningwithguardedrecursionforcoinductivetypes AT larsbirkedal theguardedlambdacalculusprogrammingandreasoningwithguardedrecursionforcoinductivetypes AT ranaldclouston guardedlambdacalculusprogrammingandreasoningwithguardedrecursionforcoinductivetypes AT alesbizjak guardedlambdacalculusprogrammingandreasoningwithguardedrecursionforcoinductivetypes AT hansbuggegrathwohl guardedlambdacalculusprogrammingandreasoningwithguardedrecursionforcoinductivetypes AT larsbirkedal guardedlambdacalculusprogrammingandreasoningwithguardedrecursionforcoinductivetypes |