Adam Chlipala, from ICFP 2008, available from Adam Chlipala’s website:

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.

Slides from Adam Chlipala’s ICFP 2008 presentation are available here.

### Like this:

Like Loading...

*Related*

I think that, to get a glimpse of each technique, it would be useful to implement a common example with each of the proposed techniques. What could be the hello-world of name binding? I suggest counting occurrences of a particular variable in open expressions of untyped lambda calculus. Here’s how to do it with the technique introduced in this paper (assuming HTML doesn’t destroy the indentation).

Sorry, CountV above always returns zero because Term is the type of closed terms. Here’s a version which accepts an open term with one variable, and which counts occurrences of that variable.

CountV : (forall var -> var -> term var) -> Nat

CountV e = countV (e Bool true)

Fabulous, what a website it is! This web site provides valuable data to us,

keep it up.