A verified staged interpreter is a verified compiler

ABSTRACT

Dependent types and multi-stage programming have both been used, separately, in programming language design and implementation. Each technique has its own advantages --- with dependent types, we can verify aspects of interpreters and compilers such as type safety and stack invariants. Multi-stage programming, on the other hand, can give the implementor access to underlying compiler technology; a staged interpreter is a translator. In this paper, we investigate the combination of these techniques. We implement an interpreter for a simply typed lambda calculus, using dependent types to guarantee correctness properties by construction. We give explicit proofs of these correctness properties, then add staging annotations to generate a translator from the interpreter. In this way, we have constructed a verified compiler from a verified staged interpreter. We illustrate the application of the technique by considering a simple staged interpreter that provides guarantees for some simple resource bound properties, as might be found in a domain specific language for real-time embedded systems.

REFERENCES

• 1: T. Altenkirch. Stop thinking about bottoms when writing programs, 2006. Talk at BCTCS 2006.
• 2: T. Altenkirch, C. McBride, and J. McKinna. Why dependent types matter. http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf, 2005. Draft.
• 3: Lennart Augustsson, Cayenne—a language with dependent types, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.239-250, September 26-29, 1998, Baltimore, Maryland, United States
• 4: L. Augustsson and M. Carlsson. An exercise in dependent types: A well-typed interpreter. http://www.cs.chalmers.se/~augustss/cayenne/, 1999.
• 5: U. Berger and H. Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In R. Vemuri, editor,Proc. 1991 IEEE Symp. on Logic in Comp. Sci., pages 203--211, 1991.
• 6: E. Brady. Practical Implementation of a Dependently Typed Functional Programming Language. PhD thesis, University of Durham, 2005.
• 7: E. Brady and K. Hammond. A dependently typed framework for static analysis of program execution costs. In Proc. Implementation of Functional Languages (IFL 2005). Springer, 2006.
• 8: L. Cardelli. Phase distinctions in type theory. Manuscript, 1988.
• 9: Coq Development Team. The Coq proof assistant --- reference manual. http://coq.inria.fr/+, 2001.
• 10: H. B. Curry and R. Feys. Combinatory Logic, volume 1. North Holland, 1958.
• 11: K. Czarnecki, J. O'Donnell, J. Striegnitz, and W. Taha. DSL implementation in MetaOCaml, Template Haskell, and C++. InDomain Specific Program Genearation 2004, volume 3016 of LNCS. Springer, 2004.
• 12: P. Dybjer. Inductive families. Formal Aspects of Computing, 6(4):440--465, 1994.
• 13: J. Eckhardt, R. Kaibachev, E. Pašalíc, K. Swadi, and W. Taha. Implicitly heterogeneous multi-stage programming. In Proc. 2005 Conf. on Generative Programming and Component Engineering (GPCE 2005), volume 3676 ofLNCS. Springer, 2005.
• 14: Yoshihiko Futamura, Partial Evaluation of Computation Process—AnApproach to a Compiler-Compiler, Higher-Order and Symbolic Computation, v.12 n.4, p.381-391, December 1999 [doi>10.1023/A:1010095604496]
• 15: Benjamin Grégoire , Xavier Leroy, A compiled implementation of strong reduction, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.235-246, October 04-06, 2002, Pittsburgh, PA, USA
• 16: Kevin Hammond , Greg Michaelson, Hume: a domain-specific language for real-time embedded systems, Proceedings of the 2nd international conference on Generative programming and component engineering, p.37-56, September 22-25, 2003, Erfurt, Germany
• 17: Robert Harper , Robert Pollack, Type checking with universes, Theoretical Computer Science, v.89 n.1, p.107-136, Oct. 21, 1991
• 18: W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors,To H.B.Curry: Essays on combinatory logic, lambda calculus and formalism. Academic Press, 1980. A reprint of an unpublished manuscript from 1969.
• 19: G. Hutton and J. Wright. Compiling exceptions correctly. InMathematics of Program Construction, volume 3125 of LNCS. Springer, 2004.
• 20: Oleg Kiselyov , Kedar N. Swadi , Walid Taha, A methodology for generating verified combinatorial circuits, Proceedings of the 4th ACM international conference on Embedded software, September 27-29, 2004, Pisa, Italy [doi>10.1145/1017753.1017794]
• 21: Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-54, January 11-13, 2006, Charleston, South Carolina, USA
• 22: Zhaohui Luo, Computation and reasoning: a type theory for computer science, Oxford University Press, Inc., New York, NY, 1994
• 23: C. McBride. Dependently Typed Functional Programs and their proofs. PhD thesis, University of Edinburgh, May 2000.
• 24: C. McBride. Epigram: Practical programming with dependent types. Lecture Notes, International Summer School on Advanced Functional Programming, 2004.
• 25: Conor McBride , James McKinna, The view from the left, Journal of Functional Programming, v.14 n.1, p.69-111, January 2004 [doi>10.1017/S0956796803004829]
• 26: James McKinna, Why dependent types matter, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-1, January 11-13, 2006, Charleston, South Carolina, USA
• 27: J. McKinna and J. Wright. A type-correct, stack-safe, provably correct expression compiler in Epigram. Journal of Functional Programming, 2006. To appear.
• 28: MetaOCaml: A compiled, type-safe multi-stage programming language. Available online from http://www.cs.rice.edu/~taha/MetaOCaml/, 2001.
• 29: E. Pašalíc. The Role of Type-Equality in Meta-programming. PhD thesis, OGI School of Science and Engineering, 2004.
• 30: Emir PašaliΕ , Walid Taha , Tim Sheard, Tagless staged interpreters for typed languages, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.218-229, October 04-06, 2002, Pittsburgh, PA, USA
• 31: Tim Sheard , Simon Peyton Jones, Template meta-programming for Haskell, Proceedings of the 2002 ACM SIGPLAN workshop on Haskell, p.1-16, October 03, 2002, Pittsburgh, Pennsylvania [doi>10.1145/581690.581691]
• 32: Walid Mohamed Taha , Tim Sheard, Multistage programming: its theory and applications, 1999
• 33: W. Taha. A gentle introduction to multi-stage programming, 2003. Available from http://www.cs.rice.edu/~taha/publications/journal/dspg04a.pdf.
• 34: W. Taha, S. Ellner, and H. Xi. Generating heap-bounded programs in a functional setting. InThird International Conference on Embedded Software, volume 2855 ofLNCS. Springer, 2003.
• 35: Walid Taha , Michael Florentin Nielsen, Environment classifiers, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.26-37, January 15-17, 2003, New Orleans, Louisiana, USA
• 36: T. Uustalu. Partiality is an effect, 2004. Talk at Dagstuhl workshop on Dependently Typed Progamming.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Interpreters

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods; Correctness proofs
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers; Translator writing systems and compiler generators

General Terms:
Languages, Theory, Verification

Keywords:
dependent types, domain specific language implementation, functional programming, multi-stage programming, partial evaluation, resource aware programming