Gallimaufry: An Automated Framework for Proving Type Soundness Part of the Constructive Logic for Automated Software Engineering Workshop.
Abstract: 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 ob ject-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.