BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Wojciech Różowski (Lean FRO)
DTSTART:20260122T150000Z
DTEND:20260122T153000Z
DTSTAMP:20260420T025630Z
UID:LT2026/31
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/31/">
 Coinductive predicates in Lean</a>\nby Wojciech Różowski (Lean FRO) as p
 art of Lean Together 2026\n\n\nAbstract\nCoinduction\, the mathematical du
 al of induction\, is a fundamental proof principle in computer science\, e
 ssential for reasoning about infinite structures\, concurrent systems\, an
 d compiler correctness. While full coinductive data support in proof assis
 tants typically requires foundational support and careful considerations\,
  such as syntactic guardedness checking\, focusing on the simpler case of 
 coinductive predicates can recover many important use cases. This is suffi
 cient for defining concepts like bisimulations and other coinductive relat
 ions crucial for program verification.\n\nThis talk presents our design an
 d implementation of coinductive predicates in Lean 4. Our approach leverag
 es lattice theory and the impredicativity of Lean's propositional universe
  to encode coinductive predicates and their proof principles directly with
 in Lean's existing type theory\, no kernel extensions required. Our implem
 entation supports mutual coinduction\, including mixed coinductive and ind
 uctive definitions. The talk will also touch on supporting syntax similar 
 to the one for usual inductive types and compiling such definitions to mon
 otone maps.\n\nJoint work with Joachim Breitner (Lean FRO\, Germany).\n
LOCATION:https://researchseminars.org/talk/LT2026/31/
END:VEVENT
END:VCALENDAR