Lambda the Ultimate

Parametric Higher-Order Abstract Syntax for Mechanized Semantics

We present parametric higher-order abstract syntax (PHOAS), a new approach to formalizing the syntax of programming languages in computer proof assistants based on type theory. Like higher-order abstract syntax (HOAS), PHOAS uses the meta language's binding constructs to represent the object language's binding constructs. Unlike HOAS, PHOAS types are definable in general-purpose type theories that support traditional functional programming, like Coq's Calculus of Inductive Constructions. We walk through how Coq can be used to develop certified, executable program transformations over several statically-typed functional programming languages formalized with PHOAS; that is, each transformation has a machine-checked proof of type preservation and semantic preservation. Our examples include CPS translation and closure conversion for simply-typed lambda calculus, CPS translation for System F, and translation from a language with ML-style pattern matching to a simpler language with no variable-arity binding constructs. By avoiding the syntactic hassle associated with first-order representation techniques, we achieve a very high degree of proof automation.

I was aware of this some months ago now, but held back commenting on it at Adam's request until it had been accepted for publication, which it now apparently has. This is (one element of) Adam's continued work on LambdaTamer, his Coq-based environment for building certified compilers. There is a new version of LambdaTamer using this parametric higher-order abstract syntax approach. The new version also works in current and future versions of Coq, unlike the previous version. Finally, Adam is apparently working on a paper regarding "type-theoretic denotational semantics for higher order, impure object languages" and is post-docing with Greg Morrisett. The relationship between Adam's work and the YNot project is a bit unclear to me; perhaps either Adam or Greg could help clarify that.

Update: Whoops. I got ahead of myself and neglected to notice that the paper is not actually yet available, although the new version of LambdaTamer is. So at the moment, this story is merely to note that the paper exists and to provide a link to the new LambdaTamer. My apologies to Adam and the LtU readership.

2nd Update: The paper is now available at the link, in either PostScript or PDF form.