Garlene: Guarded Recursion in Lean
Sergei Stepanenko, Patrick Bahr, Rasmus Ejlers Møgelberg
cs.LO
Sep 21, 2026 · v1
cs.PL
TL;DR
Implements Nakano's guarded recursion as a deep-embedded language in Lean 4 with metaprogramming, a proof mode, and a presheaf model.
Abstract
Extending the recursion principles of a formal system is an enticing but dangerous endeavour with a well-documented history of leading to consistency bugs. Nakano's guarded recursion is an elegant, type-based approach to soundly extend type theory with a powerful recursion principle. This makes guarded recursion useful for many applications, from programming with infinite structures such as streams to reasoning about advanced programming language features using synthetic guarded domain theory. Sadly, guarded recursion is not directly supported by any major interactive theorem prover, which leaves users of guarded recursion with unmechanised pen-and-paper proofs or mechanisations that depend on unmaintained theorem provers. In this paper, we present an implementation of guarded recursion as an embedded language in Lean consisting of a simply-typed lambda calculus for definitions and a higher-order logic for reasoning. Using Lean's excellent support for metaprogramming, our language allows users to write guarded recursive definitions in an intuitive syntax and to prove properties about them using a dedicated proof mode. We give our language a presheaf model, which we use to prove the soundness of our language and to allow users to export guarded recursive definitions and their theorems into standard Lean developments. To demonstrate the usefulness of our language, we present several case studies for programming and reasoning with guarded recursion.
Problem
Guarded recursion is a type-based approach to soundly extend type theory with powerful recursion, useful for programming with infinite structures and synthetic guarded domain theory. However, no major interactive theorem prover directly supports guarded recursion, leaving users with pen-and-paper proofs or unmaintained provers.
Approach
Garlene is implemented as an embedded language in Lean 4 via a deep embedding, consisting of a simply-typed lambda calculus for definitions and a higher-order logic for reasoning. Lean's metaprogramming supports intuitive user syntax elaboration and a dedicated interactive proof mode. A presheaf model (topos of trees) is used to prove soundness and to export guarded definitions and theorems into standard Lean developments. The logic is a novel Fitch-style logic with separate contexts for variables and hypotheses.
Results
Two case studies demonstrate the framework: proving the monad laws and free delay algebra characterization of the guarded delay monad, and interpreting a lambda-calculus with fixpoints in a guarded recursive domain with soundness and adequacy proofs. The mechanization is available on Zenodo and GitHub.
