4rd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory

Edinburgh, Scotland

Sponsored by ACM SIGPLAN

Co-located with ICFP’09.


Invited Talk

9:00 -- 10:00  Adam Chlipala
               Engineering a Verified Functional Language Compiler
              [abstract | slides]

Second Session

10:30 -- 11:10  Jacques Garrigue
               A Certified Interpreter for ML with Structural
              [abstract | slides]

11:20 -- 12:00  Noriko Hirota and Kenichi Asai
               Type Soundness of Lambda-Calculus with Shift/Reset 
               and Let-Polymorphism

Third Session

13:30 -- 14:10  Masahiko Sato and Randy Pollack
                A Canonical Locally Named Representation of Binding

14:20 -- 15:00  Robert Atkey
                A Deep Embedding of Parametric Polymorphism in Coq

Fourth Session

15:30 -- 16:10 Evan Austin, Aaron Stump and Edwin Westbrook
               POPLmark 1A in CINIC

16:15 -- 16:55 Sunil Kothari and James L. Caldwell
               Toward a machine-certified correctness proof of
               Wand's type reconstruction algorithm

17:00 -- 17:40 Nick Benton, Andrew Kennedy and Chung-Kil Hur
               Strongly typed term representations in Coq

Abstract for invited talk
Engineering a Verified Functional Language Compiler
Adam Chlipala

Not all binder representations are created equal.  The POPLmark
Challenge prompted a lot of consideration representations suited for
syntactic type soundness proofs and related metatheory.  Perhaps
surprisingly, other domains of mechanized proving about languages impose
different enough challenges that the "POPLmark champions" don't fare
much better than the most basic concrete binding techniques.  Compiler
verification for functional languages is one such example, and in this
talk I'll share my experiences in that area.

I will illustrate some lessons by discussing one implemented case study:
a verified compiler to an idealized assembly language from an untyped
Mini-ML with mutable references and exceptions.  This development
represents variable binders using parametric higher-order abstract
syntax, an adaptation to Coq of the "Boxes Go Bananas" technique of
Washburn and Weirich.  Higher-order representation brings some of its
usual advantages in the avoidance of binder bureaucracy, without
stepping outside of the feature set compatible with a general-purpose
type theory like Coq's.  The main body of the formal development
contains no mention of substitution or any other binder rearrangement
operation, and so there are no theorems characterizing the interaction
of such operations and the several compiler transformations.  Such
theorems have tended to make up the majority of past proofs about
compiling functional programs in multiple phases.

The streamlining of representation makes it possible to apply proof
automation quite effectively.  Every theorem is proved by an adaptive
Coq proof script.  When a new language feature has no deep effect on a
particular theorem, the proof of that theorem often continues working
verbatim for the updated language.  In implementing and proving four
main compiler phases and two optimization phases, we average under 250
lines of proof script and 800 lines of total code per phase.