4rd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory
Edinburgh, Scotland
- 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
Polymorphism
[abstract
| slides]
11:20 -- 12:00 Noriko Hirota and
Kenichi Asai
Type Soundness of Lambda-Calculus with Shift/Reset
and Let-Polymorphism
[slides]
Third Session
13:30 -- 14:10 Masahiko Sato and
Randy Pollack
A Canonical Locally Named Representation of Binding
[slides]
14:20 -- 15:00 Robert Atkey
A Deep Embedding of Parametric Polymorphism in Coq
[slides]
Fourth Session
15:30 -- 16:10 Evan
Austin, Aaron Stump and Edwin Westbrook
POPLmark 1A in CINIC
[slides]
16:15 -- 16:55 Sunil
Kothari and James L. Caldwell
Toward a machine-certified correctness proof of
Wand's type reconstruction algorithm
[slides]
17:00 -- 17:40 Nick
Benton, Andrew Kennedy and Chung-Kil Hur
Strongly typed term representations in Coq
[slides]
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.