Co-located with ICFP’09.

```
http://www.cis.upenn.edu/~sweirich/wmm/
```

- 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.