BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Recursive Definitions in Lean - Joachim Breitner\, Lean FRO
DTSTART:20250815T101500Z
DTEND:20250815T111500Z
UID:TALK234943@talks.cam.ac.uk
CONTACT:Tobias Grosser
DESCRIPTION:The log­ic un­der­ly­ing the Lean programming language and
  theorem prover does not know re­cur­sive func­tions\, yet Lean users c
 an de­fine func­tions re­cur­sive­ly. In this ses­sion we’ll get t
 o look at how Lean trans­lates the user’s spec­i­fi­ca­tion into so
 me­thing that the log­ic un­der­stands\, whether by struc­tur­al re
 ­cur­sion\, well-found­ed re­cur­sion or the brand-new par­tial fix
 ­point strat­e­gy. We’ll also see how this af­fects com­piled code 
 (name­ly not at all)\, and the dif­fer­ence be­tween par­tial and un
 ­safe.\n\n\nThis ses­sion will like­ly con­tain high amounts of im­pr
 o­vised live-cod­ing and ben­e­fit great­ly from your ques­tions\, s
 ug­ges­tions and dis­cus­sions.\n\n\nJoachim Breitner\n@nomeata\n\nEve
 r since Joachim has found beauty and elegance in Functional Programming\, 
 he’s been working with and on functional programming languages\, in part
 icular Haskell.\n\nHe’s also always been fascinated by Interactive Theor
 em Proving and his academic persona used Isabelle and Coq for formalize ma
 thematics and verify programs.\n\nThese two interests find their natural s
 ynthesis in the Lean programming language\, and Joachim joined the Lean FR
 O to work on the Lean compiler itself.\n\nBesides such serious nerdery\, y
 ou’ll find Joachim dancing Swing and Tango (in particular when traveling
  to conferences\, so talk to him if you want to join)\, paragliding and un
 apologetically making bad puns.
LOCATION:Computer Laboratory\, LT1
END:VEVENT
END:VCALENDAR