Polytypic programming in COQ

ABSTRACT

The aim of our work is to provide an infrastructure for formal proofs over Generic Haskell-style polytypic programs. For this goal to succeed, we must have a definition of polytypic programming which is both fully formal and as close as possible to the definition in Generic Haskell. In this paper we show a formalization in the proof assistant Coq of type and term specialization. Our definition of term specialization can be interpreted as a formal proof that the result of term specialization has the type computed by type specialization.

REFERENCES

• 1: Andreas Abel. Type-Based Termination of Generic Programs. Science of Computer Programming, 2007. MPC'06 special issue. Submitted.
• 2: Artem Alimarine. Generic Functional Programming: Conceptual Design, Implementation and Applications. PhD thesis, Radbound Universiteit Nijmegen, 2005.
• 3: Thorsten Altenkirch , Conor McBride, Generic Programming within Dependently Typed Programming, Proceedings of the IFIP TC2/WG2.1 Working Conference on Generic Programming, p.1-20, July 11-12, 2002
• 4: Marcin Benke , Peter Dybjer , Patrik Jansson, Universes for generic programs and proofs in dependent type theory, Nordic Journal of Computing, v.10 n.4, p.265-289, December 2003
• 5: Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
• 6: Coq Development Team. Coq frequently asked questions (v8.1), 2008. http://coq.inria.fr/doc-eng.html.
• 7: Thierry Coquand and Gérard Huet. The Calculus of Constructions. Information and Computation, 760 (2-3):0 95--120, 1988. ISSN 0890-5401. http://dx.doi.org/10.1016/0890-5401(88)90005-3.
• 8: N. G. de Bruijn. A lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 34:0 381--392, 1972.
• 9: Robert Harper , Robert Pollack, Type checking with universes, Theoretical Computer Science, v.89 n.1, p.107-136, Oct. 21, 1991
• 10: Ralf Hinze, Polytypic Values Possess Polykinded Types, Proceedings of the 5th International Conference on Mathematics of Program Construction, p.2-27, July 03-05, 2000
• 11: Ralf Hinze. Generic Programs and Proofs. Habilitationsschrift, Universität Bonn, Germany, 2000b.
• 12: Ralf Hinze, Generics for the masses, Journal of Functional Programming, v.16 n.4-5, p.451-483, July 2006 [doi>10.1017/S0956796806006022]
• 13: Ralf Hinze and Simon Peyton Jones. Derivable Type Classes. In Graham Hutton, editor, Proceedings of the 2000 ACM SIG-PLAN Haskell Workshop, Electronic Notes in Theoretical Computer Science, Volume 41.1. Elsevier Science, 2000.
• 14: Ralf Hinze and Andres Löh. Generic Programming, Now! In Roland Backhouse, Jeremy Gibbons, Ralf Hinze, and Johan Jeuring, editors, School on Datatype-Generic Programming, 2006, volume 4719 of Lecture Notes in Computer Science, pages 150--208. Springer-Verlag, 2006a.
• 15: Ralf Hinze and Andres Löh. "Scrap Your Boilerplate"' Revolutions. In Tarmo Uustalu, editor, Mathematics of Program Construction: 8th International Conference (MPC 2006), volume 4014 of Lecture Notes in Computer Science, pages 180--208. Springer-Verlag, 2006b.
• 16: Ralf Hinze, Johan Jeuring, and Andres Löh. Comparing Approaches to Generic Programming in Haskell. In Roland Backhouse, Jeremy Gibbons, Ralf Hinze, and Johan Jeuring, editors, School on Datatype-Generic Programming, 2006, volume 4719 of Lecture Notes in Computer Science, pages 72--149. Springer-Verlag, 2006a.
• 17: Ralf Hinze, Andres Löh, and Bruno Oliveira. "Scrap Your Boilerplate" Reloaded. In Proceedings of FLOPS 2006, 2006b.
• 18: Antonius J. C. Hurkens, A Simplification of Girard's Paradox, Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, p.266-278, April 10-12, 1995
• 19: Patrik Jansson , Johan Jeuring, PolyP—a polytypic programming language extension, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.470-482, January 15-17, 1997, Paris, France [doi>10.1145/263699.263763]
• 20: Ralf Lämmel , Simon Peyton Jones, Scrap your boilerplate: a practical design pattern for generic programming, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 21: Ralf Lämmel , Simon Peyton Jones, Scrap your boilerplate with class: extensible generic functions, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 22: Andres Löh. Exploring Generic Haskell. PhD thesis, Instituut voor Programmatuurkunde en Algoritmiek, 2004.
• 23: Conor McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, 1999.
• 24: Peter Morris, Thorsten Altenkirch, and Conor McBride. Exploring the Regular Tree Types. In Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors, Types for Proofs and Programs (TYPES 2004), volume 3839 of Lecture Notes in Computer Science, pages 252--267. Springer-Verlag, 2006.
• 25: Peter Morris, Thorsten Altenkirch, and Neil Ghani. Constructing Strictly Positive Families. In Joachim Gudmundsson and Barry Jay, editors, Theory of Computing (CATS 2007), Conferences in Research and Practice in Information Technology (CRPIT), Volume 65, 2007.
• 26: Ulf Norell. Functional generic programming and type theory. Master's thesis, Computing Science, Chalmers University of Technology, 2002.
• 27: Simon Peyton Jones , Dimitrios Vytiniotis , Stephanie Weirich , Geoffrey Washburn, Simple unification-based type inference for GADTs, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 28: Holger Pfeifer and Harald Rueß. Polytypic Abstraction in Type Theory. In Roland Backhouse and Tim Sheard, editors, Workshop on Generic Programming (WGP'98). June 1998.
• 29: Holger Pfeifer , Harald Rueß, Polytypic Proof Construction, Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, p.55-72, September 01, 1999
• 30: Tim Sheard. Generic Programming in mega. In Roland Backhouse, Jeremy Gibbons, Ralf Hinze, and Johan Jeuring, editors, Spring School on Datatype-Generic Programming, volume 4719 of Lecture Notes in Computer Science. Springer-Verlag, 2007.
• 31: M. H. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier, 2006.
• 32: Wendy Verbruggen. Coq sources for this paper, 2008. https://www.cs.tcd.ie/verbruwj/pub/.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

General Terms:
Languages, Theory, Verification

Keywords:
coq, formalization, generic programming, kind-indexed types, polytypic programming, theorem proving