Parametric higher-order abstract syntax for mechanized semantics Export

@article{citeulike:3823375, abstract = {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.}, address = {New York, NY, USA}, author = {Chlipala, Adam}, citeulike-article-id = {3823375}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1411203.1411226}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1411203.1411226}, doi = {10.1145/1411203.1411226}, issn = {0362-1340}, journal = {SIGPLAN Not.}, keywords = {functionalprogramming, gadt, haskell, hoas}, number = {9}, pages = {143--156}, posted-at = {2008-12-25 00:50:47}, priority = {2}, publisher = {ACM}, title = {Parametric higher-order abstract syntax for mechanized semantics}, url = {http://dx.doi.org/10.1145/1411203.1411226}, volume = {43}, year = {2008} }

TY - JOUR ID - citeulike:3823375 L3 - citeulike-article-id:3823375 N2 - 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. IS - 9 JF - SIGPLAN Not. SN - 0362-1340 AD - New York, NY, USA EP - 156 TI - Parametric higher-order abstract syntax for mechanized semantics PB - ACM VL - 43 SP - 143 KW - functionalprogramming KW - gadt KW - haskell KW - hoas AU - Chlipala, Adam PY - 2008/// UR - http://dx.doi.org/10.1145/1411203.1411226 ER -