Speaker
Horatiu Cheval
University of Bucharest
Talks at this conference:
Tuesday, 17:45, J335 
Defining and reasoning about partial (co)recursive functions in Lean 
Authors: Horatiu Cheval, David Nowak and Vlad Rusu While partial recursive functions are ubiquitous in programming,
proving results about their behavior using dependently typed proof assistants
like Coq or Lean is not straightforward, as they typically require the totality of all functions.
In this talk, we present a new approach for defining and reasoning about
potentially nonterminating functions in such systems, and a workinprogress formalization
of these methods in the Lean theorem prover.
Our framework, which is based on domain theory,
allows one to embed such partial functions and constructs like At the same time, we introduce a domaintheoretical representation of coinductive types
and partial corecursive functions.
This, together with convenient automations, provides an extension to Lean, whose native theory does
not include such notions.
Furthermore, our representation allows one to also write corecursive functions
that would normally not be accepted even in systems with builtin coinductives, like Coq,
as they would violate a required guardedness condition
(like the Bibliography
