[$LIST] I'm giving a practice talk Wednesday March 30 at 4:00 PM in 1325 CS

[mulhern <mulhern@xxxxxxxxxxx>]

Brief abstract:

<x-tad-bigger>Gallimaufry is a novel language extension development framework with an integrated type-safety component. Its core component is a translator which translates programs written in a simple object-oriented language to semantically equivalent programs in a lambda calculus. A proof of the correctness of the translator is then constructed using an automated proof assistant, Coq. A user of Gallimaufry will experiment with a language feature by specifying the syntax and translation rules for the feature. Gallimaufry will then automatically generate a proof of the type-safety of the feature or will indicate where the proof fails.</x-tad-bigger>