A certified type-preserving compiler from lambda calculus to assembly language Export

@article{citeulike:2429743, abstract = {We present a certified compiler from the simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler and the terms of its several intermediate languages are given dependent types that guarantee that only well-typed programs are representable. Thus, type preservation for each compiler pass follows without any significant "proofs" of the usual kind. Semantics preservation is proved based on denotational semantics assigned to the intermediate languages. We demonstrate how working with a type-preserving compiler enables type-directed proof search to discharge large parts of our proof obligations automatically.}, address = {New York, NY, USA}, author = {Chlipala, Adam}, citeulike-article-id = {2429743}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1273442.1250742}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1273442.1250742}, doi = {10.1145/1273442.1250742}, issn = {0362-1340}, journal = {SIGPLAN Not.}, keywords = {assembly-language, compilers, lambda-calculus, type-preserving}, month = {June}, number = {6}, pages = {54--65}, posted-at = {2008-07-24 05:30:06}, priority = {4}, publisher = {ACM}, title = {A certified type-preserving compiler from lambda calculus to assembly language}, url = {http://dx.doi.org/10.1145/1273442.1250742}, volume = {42}, year = {2007} }

TY - JOUR ID - citeulike:2429743 L3 - citeulike-article-id:2429743 N2 - We present a certified compiler from the simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler and the terms of its several intermediate languages are given dependent types that guarantee that only well-typed programs are representable. Thus, type preservation for each compiler pass follows without any significant "proofs" of the usual kind. Semantics preservation is proved based on denotational semantics assigned to the intermediate languages. We demonstrate how working with a type-preserving compiler enables type-directed proof search to discharge large parts of our proof obligations automatically. IS - 6 JF - SIGPLAN Not. SN - 0362-1340 AD - New York, NY, USA EP - 65 TI - A certified type-preserving compiler from lambda calculus to assembly language PB - ACM VL - 42 SP - 54 KW - assembly-language KW - compilers KW - lambda-calculus KW - type-preserving AU - Chlipala, Adam PY - 2007/06// UR - http://dx.doi.org/10.1145/1273442.1250742 ER -