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:TALK234940@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\nJoachim Breitner\n@nomeata\n\nEver since Joachim has found beau
 ty and elegance in Functional Programming\, he’s been working with and o
 n functional programming languages\, in particular Haskell.\n\nHe’s also
  always been fascinated by Interactive Theorem Proving and his academic pe
 rsona used Isabelle and Coq for formalize mathematics and verify programs.
 \n\nThese two interests find their natural synthesis in the Lean programmi
 ng language\, and Joachim joined the Lean FRO to work on the Lean compiler
  itself.\n\nBesides such serious nerdery\, you’ll find Joachim dancing S
 wing and Tango (in particular when traveling to conferences\, so talk to h
 im if you want to join)\, paragliding and unapologetically making bad puns
 .\n\nThis ses­sion will like­ly con­tain high amounts of im­pro­vised
  live-cod­ing and ben­e­fit great­ly from your ques­tions\, sug­ges
 ­tions and dis­cus­sions.\n\n
LOCATION:Computer Laboratory\, LT1
END:VEVENT
END:VCALENDAR