Search

• < Previous
• 1
• Next >

---

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

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&nbsp;[&hellip;]

---

Step-Indexed Relational Reasoning for Countable Nondeterminism

Lars Birkedal ; Aleš Bizjak ; Jan Schwinghammer.

Programming languages with countable nondeterministic choice are computationally interesting since countable nondeterminism arises when modeling fairness for concurrent systems. Because countable choice introduces non-continuous behaviour, it is well-known that developing semantic models for&nbsp;[&hellip;]

---