On April 4, 2024 at 14:00 EEST, Horațiu Cheval (University of Bucharest) will give a talk in the Logic Seminar.
Title: Partial (co)recursive functions in Coq and Lean
Abstract:
We present a novel method, based on domain theory, for defining partial recursive functions in interactive theorem provers like Coq and Lean, which would normally reject such definitions, as they require the termination of all functions. Our approach further extends to a representation of coinductive types and partial corecursive functions on them, which enhances the expressiveness of both systems. While Coq does contain built-in corecursion, it does not accept functions like mirror on infinitely deep trees, due to it violating the so-called guardedness condition, or filter on streams, as it is not total. Both of these can be defined in the presented encoding. Furthermore, Lean lacks entirely a native notion of coinductives, therefore the domain-theoretical representation can be used to build them from scratch in it. This is joint work with David Nowak and Vlad Rusu.
The talk will take place physically at FMI (Academiei 14), Hall 214 “Google”.