Document Open Access Logo

Typeful Normalization by Evaluation

Authors Olivier Danvy, Chantal Keller, Matthias Puech

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2014.72.pdf
  • Filesize: 0.5 MB
  • 17 pages

Document Identifiers

Subject Classification

Keywords
  • Normalization by Evaluation
  • Generalized Algebraic Data Types
  • Continuation-Passing Style
  • partial evaluation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We present the first typeful implementation of Normalization by Evaluation for the simply typed lambda-calculus with sums and control operators: we guarantee type preservation and eta-long (modulo commuting conversions), beta-normal forms using only Generalized Algebraic Data Types in a general-purpose programming language, here OCaml; and we account for sums and control operators with Continuation-Passing Style. First, we implement the standard NbE algorithm for the implicational fragment in a typeful way that is correct by construction. We then derive its call-by-value continuation-passing counterpart, that maps a lambda-term with sums and call/cc into a CPS term in normal form, which we express in a typed dedicated syntax.  Beyond showcasing the expressive power of GADTs, we emphasize that type inference gives a smooth way to re-derive the encodings of the syntax and typing of normal forms in Continuation-Passing Style.

Cite As Get BibTex

Olivier Danvy, Chantal Keller, and Matthias Puech. Typeful Normalization by Evaluation. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 72-88, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TYPES.2014.72

Author Details

Olivier Danvy
Chantal Keller
Matthias Puech

References

  1. Andreas Abel, Thierry Coquand, and Peter Dybjer. Normalization by evaluation for Martin-Löf type theory with typed equality judgements. In Jerzy Marcinkowski, editor, Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), pages 3-12, Wroclaw, Poland, July 2007. IEEE Computer Society Press. Google Scholar
  2. Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip J. Scott. Normalization by evaluation for typed lambda calculus with coproducts. In Joseph Halpern, editor, Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science, pages 203-210, Boston, Massachusetts, June 2001. IEEE Computer Society Press. Google Scholar
  3. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction-free normalization proof. In David H. Pitt, David E. Rydeheard, and Peter Johnstone, editors, Category Theory and Computer Science, number 953 in Lecture Notes in Computer Science, pages 182-199, Cambridge, UK, August 1995. Springer-Verlag. Google Scholar
  4. Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, and Benjamin Werner. A modular integration of SAT/SMT solvers to Coq through proof witnesses. In Jouannaud and Shao [45], pages 135-150. Google Scholar
  5. Kenichi Asai. On typing delimited continuations: three new solutions to the printf problem. Higher-Order and Symbolic Computation, 22(3):275-291, 2009. Google Scholar
  6. Kenichi Asai, Luminous Fennell, Peter Thiemann, and Yang Zhang. A type theoretic specification for partial evaluation. In Olaf Chitil, Andy King, and Olivier Danvy, editors, Proceedings of the 16th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP'14), pages 57-68, Canterbury, UK, September 2014. ACM Press. Google Scholar
  7. Robert Atkey, Sam Lindley, and Jeremy Yallop. Unembedding domain-specific languages. In Stephanie Weirich, editor, Proceedings of the 2nd ACM SIGPLAN Symposium on Haskell, Haskell 2009, Edinburgh, Scotland, UK, 3 September 2009, pages 37-48. ACM, 2009. Google Scholar
  8. Vincent Balat. Une étude des sommes fortes: isomorphismes et formes normales. PhD thesis, PPS, Université Denis Diderot (Paris VII), Paris, France, December 2002. Google Scholar
  9. Vincent Balat, Roberto Di Cosmo, and Marcelo P. Fiore. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In Xavier Leroy, editor, Proceedings of the Thirty-First Annual ACM Symposium on Principles of Programming Languages, SIGPLAN Notices, Vol. 39, No. 1, pages 64-76, Venice, Italy, January 2004. ACM Press. Google Scholar
  10. Vincent Balat and Olivier Danvy. Strong normalization by type-directed partial evaluation and run-time code generation. In Xavier Leroy and Atsushi Ohori, editors, Proceedings of the Second International Workshop on Types in Compilation, number 1473 in Lecture Notes in Computer Science, pages 240-252, Kyoto, Japan, March 1998. Springer-Verlag. Google Scholar
  11. Freiric Barral. Decidability for non standard conversions in typed λ-calculus. PhD thesis, Ludvig-Maximilians-Universität and Université Paul Sabatier, München, Germany and Toulouse, France, June 2008. Google Scholar
  12. Ulrich Berger. Program extraction from normalization proofs. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, number 664 in Lecture Notes in Computer Science, pages 91-106, Utrecht, The Netherlands, March 1993. Springer-Verlag. Google Scholar
  13. Ulrich Berger, Stefan Berghofer, Pierre Letouzey, and Helmut Schwichtenberg. Program extraction from normalization proofs. Studia Logica, 82(1):25-49, 2006. Google Scholar
  14. Ulrich Berger, Matthias Eberl, and Helmut Schwichtenberg. Normalization by evaluation. In Bernhard Möller and John V. Tucker, editors, Prospects for hardware foundations (NADA), number 1546 in Lecture Notes in Computer Science, pages 117-137, Berlin, Germany, 1998. Springer-Verlag. Google Scholar
  15. Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In Gilles Kahn, editor, Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 203-211, Amsterdam, The Netherlands, July 1991. IEEE Computer Society Press. Google Scholar
  16. Mathieu Boespflug. Conception d'un noyau de vérification de preuves pour le λΠ-calcul modulo. PhD thesis, École Polytechnique, Palaiseau, France, January 2011. Google Scholar
  17. Mathieu Boespflug, Maxime Dénès, and Benjamin Grégoire. Full reduction at full throttle. In Jouannaud and Shao [45], pages 362-377. Google Scholar
  18. Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. Journal of Functional Programming, 19(5):509-543, 2009. Google Scholar
  19. James Cheney and Ralf Hinze. First-class phantom types. Technical Report 1901, Computing and Information Science, Cornell University, Ithaca, New York, 2003. Google Scholar
  20. Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In James Hook and Peter Thiemann, editors, Proceedings of the 2008 ACM SIGPLAN International Conference on Functional Programming (ICFP'08), SIGPLAN Notices, Vol. 43, No. 9, pages 143-156, Victoria, British Columbia, September 2008. ACM Press. Google Scholar
  21. Thierry Coquand and Peter Dybjer. Intuitionistic model constructions and normalization proofs. Mathematical Structures in Computer Science, 7:75-94, 1997. Google Scholar
  22. Djordje Čubrić, Peter Dybjer, and Philip J. Scott. Normalization and the Yoneda embedding. Mathematical Structures in Computer Science, 8:153-192, 1998. Google Scholar
  23. Olivier Danvy. Back to direct style. Science of Computer Programming, 22(3):183-195, 1994. Google Scholar
  24. Olivier Danvy. Type-directed partial evaluation. In Guy L. Steele Jr., editor, Proceedings of the Twenty-Third Annual ACM Symposium on Principles of Programming Languages, pages 242-257, St. Petersburg Beach, Florida, January 1996. ACM Press. Google Scholar
  25. Olivier Danvy. Functional unparsing. Journal of Functional Programming, 8(6):621-625, 1998. Google Scholar
  26. Olivier Danvy. Online type-directed partial evaluation. In Masahiko Sato and Yoshihito Toyama, editors, Proceedings of the Third Fuji International Symposium on Functional and Logic Programming, pages 271-295, Kyoto, Japan, April 1998. World Scientific. Google Scholar
  27. Olivier Danvy and Peter Dybjer, editors. Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation (NBE 1998), BRICS Note Series NS-98-8, Gothenburg, Sweden, May 1998. BRICS, Department of Computer Science, Aarhus University. Available online at http://www.brics.dk/~nbe98/programme.html. Google Scholar
  28. Olivier Danvy and Andrzej Filinski. Abstracting control. In Mitchell Wand, editor, Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 151-160, Nice, France, June 1990. ACM Press. Google Scholar
  29. Olivier Danvy and Julia L. Lawall. Back to direct style II: First-class continuations. In William Clinger, editor, Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, LISP Pointers, Vol. V, No. 1, pages 299-310, San Francisco, California, June 1992. ACM Press. Google Scholar
  30. Olivier Danvy, Karoline Malmkjær, and Jens Palsberg. The essence of eta-expansion in partial evaluation. Lisp and Symbolic Computation, 8(3):209-227, 1995. Google Scholar
  31. Olivier Danvy, Karoline Malmkjær, and Jens Palsberg. Eta-expansion does The Trick. ACM Transactions on Programming Languages and Systems, 8(6):730-751, 1996. Google Scholar
  32. Olivier Danvy, Morten Rhiger, and Kristoffer Rose. Normalization by evaluation with typed abstract syntax. Journal of Functional Programming, 11(6):673-680, 2001. Google Scholar
  33. Peter Dybjer and Andrzej Filinski. Normalization and partial evaluation. In Gilles Barthe, Peter Dybjer, Luís Pinto, and João Saraiva, editors, Applied Semantics - Advanced Lectures, number 2395 in Lecture Notes in Computer Science, pages 137-192, Caminha, Portugal, September 2000. Springer-Verlag. Google Scholar
  34. Andrzej Filinski. Normalization by evaluation for the computational lambda-calculus. In Samson Abramsky, editor, Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, number 2044 in Lecture Notes in Computer Science, pages 151-165, Kraków, Poland, May 2001. Springer. Google Scholar
  35. Andrew Gacek, Dale Miller, and Gopalan Nadathur. A two-level logic approach to reasoning about computations. Journal of Automated Reasoning, 49(2):241-273, 2012. Google Scholar
  36. François Garillot and Benjamin Werner. Simple types in type theory: Deep and shallow encodings. In Klaus Schneider and Jens Brandt, editors, Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, number 4732 in Lecture Notes in Computer Science, pages 368-382, Kaiserslautern, Germany, September 2007. Springer. Google Scholar
  37. Jacques Garrigue and Didier Rémy. Ambivalent types for principal type inference with gadts. In Chung-chieh Shan, editor, Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9-11, 2013. Proceedings, volume 8301 of Lecture Notes in Computer Science, pages 257-272. Springer, 2013. Google Scholar
  38. George Gonthier. Formal proof - the four-color theorem. Notices of the AMS, 55(11):1382-1393, December 2008. Google Scholar
  39. Timothy G. Griffin. A formulae-as-types notion of control. In Paul Hudak, editor, Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 47-58, San Francisco, California, January 1990. ACM Press. Google Scholar
  40. Peter Hancock. The model of computable terms. In Danvy and Dybjer [27]. Available online at http://www.brics.dk/~nbe98/programme.html. Google Scholar
  41. John Hatcliff and Olivier Danvy. Thunks and the λ-calculus. Journal of Functional Programming, 7(3):303-319, 1997. Google Scholar
  42. Noriko Hirota and Kenichi Asai. Formalizing a correctness property of a type-directed partial evaluator. In Nils Anders Danielsson and Bart Jacobs, editors, Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Languages meets Program Verification, PLPV 2014, January 21, 2014, San Diego, California, USA, Co-located with POPL'14, pages 41-46. ACM, 2014. Google Scholar
  43. Danko Ilik. Constructive Completeness Proofs and Delimited Control. PhD thesis, École Polytechnique, Palaiseau, France, October 2010. Google Scholar
  44. Danko Ilik. A formalized type-directed partial evaluator for shift and reset. In Ugo de'Liguoro and Alexis Saurin, editors, Proceedings of the First Workshop on Control Operators and their Semantics, COS 2013, Eindhoven, The Netherlands, June 24-25, 2013, volume 127 of EPTCS, pages 86-100, 2013. Google Scholar
  45. Jean-Pierre Jouannaud and Zhong Shao, editors. Certified Programs and Proofs - First International Conference, CPP 2011, number 7086 in Lecture Notes in Computer Science, Kenting, Taiwan, December 2011. Springer. Google Scholar
  46. Oleg Kiselyov. Type-safe functional formatted IO, 2008. Web post, available at URL: http://okmij.org/ftp/typed-formatting/.
  47. Oleg Kiselyov. Typed tagless final interpreters. In Jeremy Gibbons, editor, Generic and Indexed Programming - International Spring School, SSGIP 2010, Oxford, UK, March 22-26, 2010, Revised Lectures, volume 7470 of Lecture Notes in Computer Science, pages 130-174. Springer, 2010. Google Scholar
  48. Per Martin-Löf. About models for intuitionistic type theories and the notion of definitional equality. In Proceedings of the Third Scandinavian Logic Symposium (1972), volume 82 of Studies in Logic and the Foundation of Mathematics, pages 81-109. North-Holland, 1975. Google Scholar
  49. Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambda-calculi (summary). In Rohit Parikh, editor, Logics of Programs - Proceedings, number 193 in Lecture Notes in Computer Science, pages 219-224, Brooklyn, New York, June 1985. Springer. Google Scholar
  50. Chetan R. Murthy. Extracting Constructive Content from Classical Proofs. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, 1990. Google Scholar
  51. Matthias Puech. Parametric HOAS with first-class modules. https://syntaxexclamation.wordpress.com/2014/06/27/parametric-hoas-with-first-class-modules/, 2014.
  52. John C. Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of 25th ACM National Conference, pages 717-740, Boston, Massachusetts, 1972. Google Scholar
  53. John C. Reynolds. Normalization and functor categories. In Danvy and Dybjer [27]. Available online at http://www.brics.dk/~nbe98/programme.html. Google Scholar
  54. Hongwei Xi, Chiyan Chen, and Gang Chen. Guarded recursive datatype constructors. In Greg Morrisett, editor, Proceedings of the Thirtieth Annual ACM Symposium on Principles of Programming Languages, SIGPLAN Notices, Vol. 38, No. 1, pages 224-235, New Orleans, Louisiana, January 2003. ACM Press. Google Scholar
  55. Jeremy Yallop and Oleg Kiselyov. First-class modules: hidden power and tantalizing promises. Presented at the 2010 Workshop on ML, 2010. Google Scholar
  56. Zhe Yang. Language Support for Program Generation: Reasoning, Implementation, and Applications. PhD thesis, Computer Science Department, New York University, New York, New York, August 2001. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact