Programming and Reasoning with Guarded Recursion for Coinductive Types

Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl +1

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 th…