Guillaume Allais
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Almost every programming language’s syntax includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of α-equivalence, capture avoiding substitution, typing contexts, runtime environments, and so on. In the past, implementing and reasoning about programming languages required careful handling to maintain the correct behaviour of bound variables. Modern programming languages include features that enable constraints like scope safety to be expressed in types. Nevertheless, the programmer is still forced to write the same boilerplate over again for each new implementation of a scope safe operation (e.g., renaming, substitution, desugaring, printing, etc.), and then again for correctness proofs.
We present an expressive universe of syntaxes with binding and demonstrate how to (1) implement scope safe traversals once and for all by generic programming; and (2) how to derive properties of these traversals by generic proving. Our universe description, generic traversals and proofs, and our examples have all been formalised in Agda and are available in the accompanying material.
NB. we recommend printing the paper in colour to benefit from syntax highlighting in code fragments.
Supplemental Material
- Michael Abbott, Thorsten Altenkirch, Conor McBride, and Neil Ghani. 2005. ∂ for data: Differentiating data structures. Fundamenta Informaticae 65, 1-2 (2005), 1–28. Google Scholar
Digital Library
- Andreas Abel. 2010. MiniAgda: Integrating Sized and Dependent Types. In Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers, PAR 2010, Edinburgh, UK, 15th July 2010. (EPTCS) , Ana Bove, Ekaterina Komendantskaya, and Milad Niqui (Eds.), Vol. 43. 14–28.Google ScholarCross Ref
- Andreas Abel, Alberto Momigliano, and Brigitte Pientka. 2017. POPLMark Reloaded. Proceedings of the Logical Frameworks and Meta-Languages: Theory and Practice Workshop (2017).Google Scholar
- Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. 2013. Copatterns: programming infinite structures by observations. In ACM SIGPLAN Notices, Vol. 48. ACM, 27–38. Google ScholarDigital Library
- Guillaume Allais, James Chapman, Conor McBride, and James McKinna. 2017. Type-and-scope Safe Programs and Their Proofs. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017). ACM, 195–207. Google ScholarDigital Library
- Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. 2010. Monads Need Not Be Endofunctors. Springer, 297–311. Google ScholarDigital Library
- Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. 2014. Relative Monads Formalised. Journal of Formalized Reasoning 7, 1 (2014), 1–43.Google Scholar
- Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. 1995. Categorical reconstruction of a reduction free normalization proof. In LNCS, Vol. 530. Springer, 182–199. Google ScholarDigital Library
- Thorsten Altenkirch and Conor McBride. 2003. Generic Programming Within Dependently Typed Programming. In Proceedings of the IFIP TC2/WG2.1 Working Conference on Generic Programming . Kluwer, B.V., 1–20. http://dl.acm.org/ citation.cfm?id=647100.717294 Google ScholarDigital Library
- Thorsten Altenkirch and Bernhard Reus. 1999. Monadic presentations of lambda terms using generalized inductive types. In CSL. Springer, 453–468. Google ScholarDigital Library
- Robert Atkey. 2015. An Algebraic Approach to Typechecking and Elaboration. (2015). http://bentnib.org/posts/ 2015-04-19-algebraic-approach-typechecking-and-elaboration.htmlGoogle Scholar
- Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. 2005. Mechanized Metatheory for the Masses: The PoplMark Challenge. In Theorem Proving in Higher Order Logics, Joe Hurd and Tom Melham (Eds.). Springer, 50–65. Google ScholarDigital Library
- Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, and Eelco Visser. 2018. Intrinsically-typed Definitional Interpreters for Imperative Languages. Proc. ACM Program. Lang. 2, POPL, Article 16 (Jan. 2018), 34 pages. Google ScholarDigital Library
- Françoise Bellegarde and James Hook. 1994. Substitution: A formal methods case study using monads and transformations. Science of Computer Programming 23, 2 (1994), 287 – 311. Google ScholarDigital Library
- Marcin Benke, Peter Dybjer, and Patrik Jansson. 2003. Universes for Generic Programs and Proofs in Dependent Type Theory. Nordic J. of Computing 10, 4 (Dec. 2003), 265–289. http://dl.acm.org/citation.cfm?id=985799.985801 Google ScholarDigital Library
- Nick Benton, Chung-Kil Hur, Andrew J Kennedy, and Conor McBride. 2012. Strongly typed term representations in Coq. JAR 49, 2 (2012), 141–159. Google ScholarDigital Library
- Richard S. Bird and Ross Paterson. 1999. de Bruijn notation as a nested datatype. Journal of Functional Programming 9, 1 (1999), 77–91. Google ScholarDigital Library
- Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 5 (2013), 552–593.Google ScholarCross Ref
- James Chapman, Pierre-Évariste Dagand, Conor McBride, and Peter Morris. 2010. The Gentle Art of Levitation. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP ’10) . ACM, 3–14. Google ScholarDigital Library
- James Maitland Chapman. 2009. Type checking and normalisation. Ph.D. Dissertation. University of Nottingham (UK).Google Scholar
- Arthur Charguéraud. 2012. The Locally Nameless Representation. Journal of Automated Reasoning 49, 3 (01 Oct 2012), 363–408.Google ScholarCross Ref
- Adam Chlipala. 2008. Parametric higher-order abstract syntax for mechanized semantics. In ACM Sigplan Notices, Vol. 43. ACM, 143–156. Google ScholarDigital Library
- Ernesto Copello. 2017. On the Formalisation of the Metatheory of the Lambda Calculus and Languages with Binders. Ph.D. Dissertation. Universidad de la República (Uruguay).Google Scholar
- Catarina Coquand. 2002. A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions. Higher-Order and Symbolic Computation 15, 1 (2002), 57–90. Google ScholarDigital Library
- Nicolaas Govert de Bruijn. 1972. Lambda Calculus Notation with Nameless Dummies. In Indagationes Mathematicae, Vol. 75. Elsevier, 381–392.Google Scholar
- Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings (Lecture Notes in Computer Science) , Amy P. Felty and Aart Middeldorp (Eds.), Vol. 9195. Springer, 378–388.Google ScholarCross Ref
- Peter Dybjer. 1994. Inductive families. Formal aspects of computing 6, 4 (1994), 440–465.Google Scholar
- Peter Dybjer and Anton Setzer. 1999. A Finite Axiomatization of Inductive-Recursive Definitions. Springer, 129–146. Google ScholarDigital Library
- Gergő Érdi. 2018. Generic description of well-scoped, well-typed syntaxes. (2018). https://github.com/gergoerdi/ universe-of-syntax Unpublished draft, privately communicated.Google Scholar
- Marcelo Fiore, Gordon Plotkin, and Daniele Turi. 1999. Abstract Syntax and Variable Binding (Extended Abstract). In Proc. 14 th LICS Conf. IEEE, Computer Society Press, 193–202. Google ScholarDigital Library
- Murdoch J. Gabbay and Andrew M. Pitts. 2001. A New Approach to Abstract Syntax with Variable Binding . 13, 3–5 (July 2001), 341–363. Google ScholarDigital Library
- Neil Ghani, Makoto Hamana, Tarmo Uustalu, and Varmo Vene. 2006. Representing cyclic structures as nested datatypes. In Proc. of 7th Symp. on Trends in Functional Programming, TFP , Vol. 2006.Google Scholar
- Makoto Hamana. 2009. Initial Algebra Semantics for Cyclic Sharing Structures. Springer, 127–141. Google ScholarDigital Library
- Paul Hudak. 1996. Building domain-specific embedded languages. ACM Computing Surveys (CSUR) 28, 4es (1996), 196. Google ScholarDigital Library
- Gérard Huet. 1997. The Zipper. Journal of Functional Programming 7, 5 (1997), 549–554. Google ScholarDigital Library
- Alan Jeffrey. 2011. Associativity for free! http://thread.gmane.org/gmane.comp.lang.agda/3259 . (2011).Google Scholar
- Jonas Kaiser, Steven Schäfer, and Kathrin Stark. 2018. Binder Aware Recursion over Well-scoped De Bruijn Syntax. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018) . ACM, 293–306. Google ScholarDigital Library
- Andrew W. Keep and R. Kent Dybvig. 2013. A Nanopass Framework for Commercial Compiler Development. SIGPLAN Not. 48, 9 (Sept. 2013), 343–350. Google ScholarDigital Library
- Steven Keuchel, Stephanie Weirich, and Tom Schrijvers. 2016. Needle & Knot: Binder Boilerplate Tied Up. In Proceedings of the 25th European Symposium on Programming Languages and Systems - Volume 9632 . Springer-Verlag New York, Inc., 419–445.Google ScholarDigital Library
- Gyesik Lee, Bruno C. D. S. Oliveira, Sungkeun Cho, and Kwangkeun Yi. 2012. GMeta: A Generic Formal Metatheory Framework for First-Order Representations. In Programming Languages and Systems, Helmut Seidl (Ed.). Springer, 436–455. Google ScholarDigital Library
- Per Martin-Löf. 1982. Constructive mathematics and computer programming. Studies in Logic and the Foundations of Mathematics 104 (1982), 153–175.Google ScholarCross Ref
- The Coq Development Team. 2017. The Coq proof assistant reference manual. π r 2 Team. http://coq.inria.fr Version 8.6.Google Scholar
- Conor McBride. 2017. Ornamental algebras, algebraic ornaments. (2017). https://personal.cis.strath.ac.uk/conor.mcbride/ pub/OAAO/Ornament.pdfGoogle Scholar
- Conor McBride and Ross Paterson. 2008. Applicative programming with effects. Journal of Functional Programming 18, 1 (2008), 1–13. Google ScholarDigital Library
- Craig McLaughlin, James McKinna, and Ian Stark. 2018. Triangulating Context Lemmas. In Proceedings of the 7th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2018) . ACM, 102–114. Google ScholarDigital Library
- John C Mitchell and Eugenio Moggi. 1991. Kripke-style models for typed lambda calculus. Annals of Pure and Applied Logic 51, 1-2 (1991), 99–124.Google ScholarCross Ref
- Peter Morris, Thorsten Altenkirch, and Conor McBride. 2006. Exploring the Regular Tree Types. In Types for Proofs and Programs , Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner (Eds.). Springer, 252–267. Google ScholarDigital Library
- Ulf Norell. 2009. Dependently typed programming in Agda. In AFP Summer School. Springer, 230–266. Google ScholarDigital Library
- Matthew Pickering, Gergő Érdi, Simon Peyton Jones, and Richard A. Eisenberg. 2016. Pattern Synonyms. In Proceedings of the 9th International Symposium on Haskell (Haskell 2016) . ACM, 80–91. Google ScholarDigital Library
- Benjamin C Pierce and David N Turner. 2000. Local type inference. ACM Transactions on Programming Languages and Systems (TOPLAS) 22, 1 (2000), 1–44. Google ScholarDigital Library
- Emmanuel Polonowski. 2013. Automatically Generated Infrastructure for De Bruijn Syntaxes. In Interactive Theorem Proving, Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer, 402–417. Google ScholarDigital Library
- Wouter Swiestra. 2008. Data types à la carte. Journal of Functional Programming 18, 4 (2008), 423–436. Google ScholarDigital Library
- David Thibodeau, Alberto Momigliano, and Brigitte Pientka. 2016. A case-study in programming coinductive proofs: Howe’s method . Technical Report. Technical report, McGill University.Google Scholar
Index Terms
- A type and scope safe universe of syntaxes with binding: their semantics and proofs
Recommendations
Type-and-scope safe programs and their proofs
CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and ProofsWe abstract the common type-and-scope safe structure from computations on λ-terms that deliver, e.g., renaming, substitution, evaluation, CPS-transformation, and printing with a name supply. By exposing this structure, we can prove generic simulation ...
Type theory in type theory using quotient inductive types
POPL '16We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids ...
Decidability of conversion for type theory in type theory
Type theory should be able to handle its own meta-theory, both to justify its foundational claims and to obtain a verified implementation. At the core of a type checker for intensional type theory lies an algorithm to check equality of types, or in ...
Comments