BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Coinductive predicates in Lean - Wojciech Różowski\, Lean FRO
DTSTART:20251002T103000Z
DTEND:20251002T113000Z
UID:TALK236845@talks.cam.ac.uk
CONTACT:120490
DESCRIPTION:Coinduction\, the mathematical dual of induction\, is a fundam
 ental proof principle in computer science\, essential for reasoning about 
 infinite structures\, concurrent systems\, and compiler correctness. While
  full coinductive data support in proof assistants typically requires foun
 dational support and careful considerations\, such as syntactic guardednes
 s checking\, focusing on the simpler case of coinductive predicates can re
 cover many important use cases. This is sufficient for defining concepts l
 ike bisimulations and other coinductive relations crucial for program veri
 fication.\n\nThis talk presents our design and implementation of coinducti
 ve predicates in Lean 4. Our approach leverages lattice theory and the imp
 redicativity of Lean's propositional universe to encode coinductive predic
 ates and their proof principles directly within Lean's existing type theor
 y\, no kernel extensions required. Our implementation supports mutual coin
 duction\, including mixed coinductive and inductive definitions. The talk 
 will also touch on supporting syntax similar to the one for usual inductiv
 e types and compiling such definitions to monotone maps.\n\nJoint work wit
 h Joachim Breitner (Lean FRO\, Germany).\n\nBio:\nWojciech Różowski is a
  Research Software Engineer at Lean FRO\, where he works on the developmen
 t of the Lean theorem prover. His research interests include automated rea
 soning\, formal semantics\, and program verification. He obtained his PhD 
 at University College London under the supervision of Alexandra Silva\, as
  a member of the Programming Principles\, Logic and Verification Group.
LOCATION:Computer Laboratory\, William Gates Building\, Lecture Theatre 2
END:VEVENT
END:VCALENDAR