3 papers
cs.LO2026
Garlene: Guarded Recursion in Lean
Sergei Stepanenko, Patrick Bahr, Rasmus Ejlers Møgelberg
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 recursi…
cs.LO2026
Iris in Lean
Markus de Medeiros, Sergei Stepanenko, Zongyuan Liu +9
The Iris framework for concurrent separation logic has been widely used for program verification research. An important factor contributing to the framework's adoption is its high-…
cs.LO2025
Context-Dependent Effects and Concurrency in Guarded Interaction Trees
Sergei Stepanenko, Emma Nardino, Virgil Marionneau +3
Guarded Interaction Trees are a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Rocq. We present an extension of…