BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:A Verified Compiler from Isabelle/HOL to CakeML
DTSTART:20181218T150000
DTEND:20181218T160000
DTSTAMP:20260414T181439Z
UID:bf6eacaf7f91e7d2dbe1060a1dc00ad181402d7164afefd5af98f78a
CATEGORIES:Conferences - Seminars
DESCRIPTION:By Lars Hupel\, Technical University of Munich\n\nAbstract\nMa
 ny theorem provers can generate functional programs from definitions or pr
 oofs. However\, this code generation needs to be trusted. Except for the H
 OL4 system\, which has a proof producing code generator for a subset of ML
 . We go one step further and provide a verified compiler from Isabelle/HOL
  to CakeML. More precisely we combine a simple proof producing translation
  of recursion equations in Isabelle/HOL into a deeply embedded term langua
 ge with a fully verified compilation chain to the target language CakeML\,
  a verified functional programming language and an ecosystem of proofs and
  tools built around the language.\n\nBio\nLars Hupel is a PhD student at 
 TU München in the field of logic and verification. His research focus 
 is on techniques for verified code generation from theorem provers. Additi
 onally\, he has worked on formal treatments of Linux firewalls. A frequent
  conference speaker and co-founder of the Typelevel initiative\, he is ac
 tive in the open source community\, particularly in Scala. He also enjoy
 s programming in Haskell\, Prolog\, and Rust.\n\nMore information\n\n\n\n
  
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR