Parametric higher-order abstract syntax

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.

4 Responses to “Parametric higher-order abstract syntax”

  1. 1 Samuel Gélineau October 4, 2009 at 10:41 pm

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

    -- first, define lambda calculus terms
    data term (var : Set) : Set where
      ref : var -> term var
      lam : (var -> term var) -> term var
      app : term var -> term var -> term var
    Term : Set
    Term = forall var -> term var
    -- next, count the variable occurrences.
    countV : term Bool -> Nat
    countV (ref true)  = 1
    countV (ref false) = 0
    countV (lam body) = countV (body false)
    countV (app e1 e2) = countV e1 + countV e2
    CountV : Term -> Nat
    CountV e = countV (e Bool)
    • 2 Samuel Gélineau October 4, 2009 at 10:49 pm

      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)

  2. 3 Danielle December 26, 2015 at 7:58 am

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

  1. 1 A verified compiler for an impure functional language « Name binding blog Trackback on January 15, 2010 at 11:52 am

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: