BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Scientific Computing in Lean - Tomas Skrivan (Carnegie Mellon Univ
 ersity)
DTSTART:20240509T160000Z
DTEND:20240509T170000Z
UID:TALK216106@talks.cam.ac.uk
CONTACT:Jonas Bayer
DESCRIPTION:The language of science is mathematics" and Lean speaks mathem
 atics. Since Lean 4 is an interactive theorem prover and general-purpose p
 rogramming language simultaneously\, it is only natural to explore its use
  for scientific computing.\n\nAt first glance\, the advantage of using Lea
 n is that we can fully formalize and prove the correctness of our programs
 . However\, we will show that the utility of using an interactive theorem 
 prover goes far beyond that. The ability to express abstract mathematical 
 concepts allows us to build a library with an extremely high level of comp
 osability. We utilize Lean's interactivity and tactic mode to create an in
 teractive computer algebra system\, perform source code transformations\, 
 or execute compiler optimization passes. Lean's extensible syntax allows u
 s to define custom domain-specific languages supporting features like prob
 abilistic programming or write programs that are guaranteed to be differen
 tiable.\n\nIn the past\, many specialized domain-specific languages have b
 een developed to support one of these features. Our aim is to develop a la
 nguage/library where all these specialized features can coexist seamlessly
 .\n\n—-\n\nWATCH ONLINE HERE: https://www.microsoft.com/en-gb/microsoft-
 teams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a5
LOCATION:Live-streamed at MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR