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...

Popoln opis

Bibliografske podrobnosti

Principais autores:	Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, Lars Birkedal
Format:	Artigo
Jezik:	Inglês
Izdano:	Logical Methods in Computer Science e.V. 2017-04-01
Serija:	Logical Methods in Computer Science
Teme:	computer science - logic in computer science computer science - programming languages
Online dostop:	https://lmcs.episciences.org/2019/pdf
Oznake:	Označite Brez oznak, prvi označite!