Document Open Access Logo

Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper)

Author Dale Miller

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2016.1.pdf
  • Filesize: 401 kB
  • 16 pages

Document Identifiers

Author Details

Dale Miller

Cite As Get BibTex

Dale Miller. Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper). In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 1:1-1:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.TYPES.2016.1

Abstract

Proof assistants and the programming languages that implement them need to deal with a range of linguistic expressions that involve bindings. Since most mature proof assistants do not have built-in methods to treat this aspect of syntax, many of them have been extended with various packages and libraries that allow them to encode bindings using, for example, de Bruijn numerals and nominal logic features. I put forward the argument that bindings are such an intimate aspect of the structure of expressions that they should be accounted for directly in the underlying programming language support for proof assistants and not added later using packages and libraries. One possible approach to designing programming languages and proof assistants that directly supports such an approach to bindings in syntax is presented. The roots of such an approach can be found in the mobility of binders between term-level bindings, formula-level bindings (quantifiers), and proof-level bindings (eigenvariables). In particular, by combining Church's approach to terms and formulas (found in his Simple Theory of Types) and Gentzen's approach to sequent calculus proofs, we can learn how bindings can declaratively interact with the full range of logical connectives and quantifiers. I will also illustrate how that framework provides an intimate and semantically clean treatment of computation and reasoning with syntax containing bindings. Some implemented systems, which support this intimate and built-in treatment of bindings, will be briefly described.

Subject Classification

Keywords
  • mechanized metatheory
  • mobility of binders
  • lambda-tree syntax
  • higher-order abstract syntax

Metrics

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

References

  1. Beniamino Accattoli. Proof pearl: Abella formalization of lambda calculus cube property. In Chris Hawblitzel and Dale Miller, editors, Second International Conference on Certified Programs and Proofs, volume 7679 of Lecture Notes in Computer Science, pages 173-187. Springer, 2012. Google Scholar
  2. Andrew W. Appel and Amy P. Felty. Polymorphic lemmas and definitions in λProlog and Twelf. Theory and Practice of Logic Programming, 4(1-2):1-39, 2004. URL: http://dx.doi.org/10.1017/S1471068403001698.
  3. Brian Aydemir, Aaron Bohannon, and Stephanie Weirich. Nominal reasoning techniques in Coq. In International Workshop on Logical Frameworks and Meta-Languages:Theory and Practice (LFMTP), pages 69-77, Seattle, WA, USA, 2006. Google Scholar
  4. Brian Aydemir, Stephan A. Zdancewic, and Stephanie Weirich. Abstracting syntax. Technical Report MS-CIS-09-06, University of Pennsylvania, 2009. Google Scholar
  5. Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The POPLmark challenge. In Theorem Proving in Higher Order Logics: 18th International Conference, number 3603 in Lecture Notes in Computer Science, pages 50-65. Springer, 2005. Google Scholar
  6. Brian E. Aydemir, Aaron Bohannon, and Stephanie Weirich. Nominal reasoning techniques in Coq: (extended abstract). Electr. Notes Theor. Comput. Sci, 174(5):69-77, 2007. URL: http://dx.doi.org/10.1016/j.entcs.2007.01.028.
  7. David Baelde. Least and greatest fixed points in linear logic. ACM Trans. on Computational Logic, 13(1), 2012. URL: http://dx.doi.org/10.1145/2071368.2071370.
  8. David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. Abella: A system for reasoning about relational specifications. Journal of Formalized Reasoning, 7(2), 2014. URL: http://dx.doi.org/10.6092/issn.1972-5787/4650.
  9. David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. The Bedwyr system for model checking over syntactic expressions. In F. Pfenning, editor, 21th Conf. on Automated Deduction (CADE), number 4603 in Lecture Notes in Artificial Intelligence, pages 391-397, New York, 2007. Springer. URL: http://dx.doi.org/10.1007/978-3-540-73595-3_28.
  10. Ulrich Berger, Stefan Berghofer, Pierre Letouzey, and Helmut Schwichtenberg. Program extraction from normalization proofs. Studia Logica, 82(1):25-49, 2006. URL: http://dx.doi.org/10.1007/s11225-006-6604-5.
  11. Filippo Bonchi and Damien Pous. Checking NFA equivalence with bisimulations up to congruence. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 457-468. ACM, 2013. Google Scholar
  12. Arthur Charguéraud. The locally nameless representation. Journal of Automated Reasoning, pages 1-46, 2011. URL: http://dx.doi.org/10.1007/s10817-011-9225-2.
  13. Kaustuv Chaudhuri, Matteo Cimini, and Dale Miller. A lightweight formalization of the metatheory of bisimulation-up-to. In Xavier Leroy and Alwen Tiu, editors, Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs, pages 157-166, Mumbai, India, 2015. ACM. URL: http://dx.doi.org/10.1145/2676724.2693170.
  14. James Cheney and Christian Urban. Nominal logic programming. ACM Trans. Program. Lang. Syst., 30(5):1-47, 2008. URL: http://dx.doi.org/10.1145/1387673.1387675.
  15. Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. In James Hook and Peter Thiemann, editors, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008, pages 143-156. ACM, 2008. URL: http://dx.doi.org/10.1145/1411204.1411226.
  16. Alonzo Church. A formulation of the Simple Theory of Types. J. of Symbolic Logic, 5:56-68, 1940. URL: http://dx.doi.org/10.2307/2266170.
  17. Dominique Clément, Joëlle Despeyroux, Thierry Despeyroux, Laurent Hascoët, and Gilles Kahn. Natural semantics on the computer. Research Report 416, INRIA, Rocquencourt, France, 1985. Google Scholar
  18. Robert L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986. Google Scholar
  19. Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76(2/3):95-120, / 1988. Google Scholar
  20. N. G. de Bruijn. A survey of the project AUTOMATH. In J. P. Seldin and R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pages 589-606. Academic Press, New York, 1980. Google Scholar
  21. Nicolaas Govert de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with an application to the Church-Rosser theorem. Indagationes Mathematicae, 34(5):381-392, 1972. Google Scholar
  22. Joëlle Despeyroux, Amy Felty, and Andre Hirschowitz. Higher-order abstract syntax in Coq. In Second International Conference on Typed Lambda Calculi and Applications, pages 124-138, apr 1995. Google Scholar
  23. Cvetan Dunchev, Claudio Sacerdoti Coen, and Enrico Tassi. Implementing HOL in an higher order logic programming language. In Gilles Dowek, Daniel R. Licata, and Sandra Alves, editors, Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2016, Porto, Portugal, June 23, 2016, pages 4:1-4:10. ACM, 2016. URL: http://dx.doi.org/10.1145/2966268.2966272.
  24. Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. ELPI: fast, embeddable, λProlog interpreter. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science, pages 460-468. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-48899-7_32.
  25. Amy Felty and Dale Miller. Specifying theorem provers in a higher-order logic programming language. In Ninth International Conference on Automated Deduction, number 310 in Lecture Notes in Computer Science, pages 61-80, Argonne, IL, may 1988. Springer. Google Scholar
  26. Amy Felty and Dale Miller. Encoding a dependent-type λ-calculus in a logic programming language. In Mark Stickel, editor, Proceedings of the 1990 Conference on Automated Deduction, volume 449 of Lecture Notes in Artificial Intelligence, pages 221-235. Springer, 1990. Google Scholar
  27. Amy Felty and Alberto Momigliano. Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax. J. of Automated Reasoning, 48:43-105, 2012. Google Scholar
  28. Amy P. Felty, Alberto Momigliano, and Brigitte Pientka. The next 700 challenge problems for reasoning with higher-order abstract syntax representations: Part 2-A survey. J. of Automated Reasoning, 55(4):307-372, 2015. Google Scholar
  29. M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax involving binders. In 14th Symp. on Logic in Computer Science, pages 214-224. IEEE Computer Society Press, 1999. Google Scholar
  30. Andrew Gacek. The Abella interactive theorem prover (system description). In A. Armando, P. Baumgartner, and G. Dowek, editors, Fourth International Joint Conference on Automated Reasoning, volume 5195 of Lecture Notes in Computer Science, pages 154-161. Springer, 2008. URL: http://arxiv.org/abs/0803.2305.
  31. Andrew Gacek, Dale Miller, and Gopalan Nadathur. Reasoning in Abella about structural operational semantics specifications. In A. Abel and C. Urban, editors, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008), number 228 in Electronic Notes in Theoretical Computer Science, pages 85-100, 2008. URL: http://dx.doi.org/10.1016/j.entcs.2008.12.118.
  32. Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Information and Computation, 209(1):48-73, 2011. URL: http://dx.doi.org/10.1016/j.ic.2010.09.004.
  33. Andrew Gacek, Dale Miller, and Gopalan Nadathur. A two-level logic approach to reasoning about computations. J. of Automated Reasoning, 49(2):241-273, 2012. URL: http://dx.doi.org/10.1007/s10817-011-9218-1.
  34. Ulysse Gérard and Dale Miller. Separating functional computation from relations. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of LIPIcs, pages 23:1-23:17, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2017.23.
  35. Kurt Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte der Mathematischen Physik, 38:173-198, 1931. English Version in [84]. Google Scholar
  36. M. J. C. Gordon and T. F. Melham. Introduction to HOL - A theorem proving environment for higher order logic. Cambridge University Press, 1993. Google Scholar
  37. Michael J. Gordon, Arthur J. Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer, 1979. Google Scholar
  38. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, 1993. Google Scholar
  39. Martin Hofmann. Semantical analysis of higher-order abstract syntax. In 14th Symp. on Logic in Computer Science, pages 204-213. IEEE Computer Society Press, 1999. Google Scholar
  40. Furio Honsell, Marino Miculan, and Ivan Scagnetto. π-calculus in (co)inductive type theories. Theoretical Computer Science, 2(253):239-285, 2001. Google Scholar
  41. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. In Proceedings of the 22nd Symposium on Operating Systems Principles (22nd SOSP'09), Operating Systems Review (OSR), pages 207-220, Big Sky, MT, 2009. ACM SIGOPS. Google Scholar
  42. Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107-115, 2009. URL: http://dx.doi.org/10.1145/1538788.1538814.
  43. Chuck Liang, Gopalan Nadathur, and Xiaochu Qi. Choices in representing and reduction strategies for lambda terms in intensional contexts. Journal of Automated Reasoning, 33:89-132, 2005. Google Scholar
  44. Donald MacKenzie. Mechanizing Proof. MIT Press, 2001. Google Scholar
  45. Per Martin-Löf. Intuitionistic Type Theory. Studies in Proof Theory Lecture Notes. Bibliopolis, Napoli, 1984. Google Scholar
  46. Raymond McDowell and Dale Miller. A logic for reasoning with higher-order abstract syntax. In Glynn Winskel, editor, 12th Symp. on Logic in Computer Science, pages 434-445, Warsaw, Poland, 1997. IEEE Computer Society Press. Google Scholar
  47. Raymond McDowell and Dale Miller. Cut-elimination for a logic with definitions and induction. Theoretical Computer Science, 232:91-119, 2000. URL: http://dx.doi.org/10.1016/S0304-3975(99)00171-1.
  48. Raymond McDowell and Dale Miller. Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. on Computational Logic, 3(1):80-136, 2002. Google Scholar
  49. Dale Miller. An extension to ML to handle bound variables in data structures: Preliminary report. In Proceedings of the Logical Frameworks BRA Workshop, pages 323-335, Antibes, France, jun 1990. Available as UPenn CIS technical report MS-CIS-90-59. URL: http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/mll.pdf.
  50. Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. J. of Logic and Computation, 1(4):497-536, 1991. Google Scholar
  51. Dale Miller. Bindings, mobility of bindings, and the ∇-quantifier. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, 18th International Conference on Computer Science Logic (CSL) 2004, volume 3210 of Lecture Notes in Computer Science, page 24, 2004. Google Scholar
  52. Dale Miller. Finding unity in computational logic. In Proceedings of the 2010 ACM-BCS Visions of Computer Science Conference, ACM-BCS '10, pages 3:1-3:13. British Computer Society, apr 2010. URL: http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/unity2010.pdf.
  53. Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, jun 2012. URL: http://dx.doi.org/10.1017/CBO9781139021326.
  54. Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125-157, 1991. Google Scholar
  55. Dale Miller and Alwen Tiu. A proof theory for generic judgments. ACM Trans. on Computational Logic, 6(4):749-783, oct 2005. URL: http://dx.doi.org/10.1145/1094622.1094628.
  56. Robin Milner. Communication and Concurrency. Prentice-Hall International, 1989. Google Scholar
  57. Robin Milner. Communicating and Mobile Systems: The π-Calculus. Cambridge University Press, New York, NY, USA, 1999. Google Scholar
  58. Alberto Momigliano and Alwen Tiu. Induction and co-induction in sequent calculus. In Mario Coppo, Stefano Berardi, and Ferruccio Damiani, editors, Post-proceedings of TYPES 2003, number 3085 in Lecture Notes in Computer Science, pages 293-308, jan 2003. Google Scholar
  59. J. Strother Moore. A mechanically verified language implementation. J. of Automated Reasoning, 5(4):461-492, 1989. Google Scholar
  60. Gopalan Nadathur and Dustin J. Mitchell. System description: Teyjus - A compiler and abstract machine based implementation of λProlog. In H. Ganzinger, editor, 16th Conf. on Automated Deduction (CADE), number 1632 in Lecture Notes in Artificial Intelligence, pages 287-291, Trento, 1999. Springer. Google Scholar
  61. Gopalan Nadathur and Debra Sue Wilson. A notation for lambda terms: A generalization of environments. Theoretical Computer Science, 198(1-2):49-98, 1998. Google Scholar
  62. Lawrence C. Paulson. A generic tableau prover and its integration with isabelle. J. UCS, 5(3):73-87, 1999. URL: http://www.jucs.org/jucs_5_3/a_generic_tableau_prover.
  63. Alan J. Perlis. Epigrams on programming. ACM SIGPLAN Notices, pages 7-13, 1982. URL: http://dx.doi.org/10.1145/947955.1083808.
  64. Frank Pfenning. Logic programming in the LF logical framework. In Gérard Huet and Gordon D. Plotkin, editors, Logical Frameworks, pages 149-181. Cambridge University Press, 1991. Google Scholar
  65. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pages 199-208. ACM Press, jun 1988. Google Scholar
  66. Frank Pfenning and Carsten Schürmann. System description: Twelf - A meta-logical framework for deductive systems. In H. Ganzinger, editor, 16th Conf. on Automated Deduction (CADE), number 1632 in Lecture Notes in Artificial Intelligence, pages 202-206, Trento, 1999. Springer. URL: http://dx.doi.org/10.1007/3-540-48660-7_14.
  67. Brigitte Pientka and Joshua Dunfield. Beluga: A framework for programming and reasoning with deductive systems (system description). In J. Giesl and R. Hähnle, editors, Fifth International Joint Conference on Automated Reasoning, number 6173 in Lecture Notes in Computer Science, pages 15-21, 2010. Google Scholar
  68. The POPLmark Challenge webpage. http://www.seas.upenn.edu/~plclub/poplmark/, 2015.
  69. François Pottier. An overview of Cαml. In ACM Workshop on ML, Electronic Notes in Theoretical Computer Science, pages 27-51, sep 2005. Google Scholar
  70. Damien Pous. Weak bisimulation upto elaboration. In C. Baier and H. Hermanns, editors, CONCUR, volume 4137 of Lecture Notes in Computer Science, pages 390-405. Springer, 2006. Google Scholar
  71. Damien Pous. Complete lattices and upto techniques. In Zhong Shao, editor, APLAS, volume 4807 of Lecture Notes in Computer Science, pages 351-366, Singapore, 2007. Springer. Google Scholar
  72. Damien Pous and Davide Sangiorgi. Enhancements of the bisimulation proof method. In Davide Sangiorgi and Jan Rutten, editors, Advanced Topics in Bisimulation and Coinduction, pages 233-289. Cambridge University Press, 2011. URL: http://dx.doi.org/10.1017/CBO9780511792588.007.
  73. Xiaochu Qi, Andrew Gacek, Steven Holte, Gopalan Nadathur, and Zach Snow. The Teyjus system - version 2, 2015. URL: http://teyjus.cs.umn.edu/.
  74. Davide Sangiorgi. π-calculus, internal mobility and agent-passing calculi. Theoretical Computer Science, 167(2):235-274, 1996. Google Scholar
  75. Helmut Schwichtenberg. Minlog. In Freek Wiedijk, editor, The Seventeen Provers of the World, volume 3600 of Lecture Notes in Computer Science, pages 151-157. Springer, 2006. URL: http://dx.doi.org/10.1007/11542384_19.
  76. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša. Ott: Effective tool support for the working semanticist. Journal of Functional Programming, 20(01):71-122, 2010. Google Scholar
  77. Zachary Snow, David Baelde, and Gopalan Nadathur. A meta-programming approach to realizing dependently typed logic programming. In Temur Kutsia, Wolfgang Schreiner, and Maribel Fernández, editors, ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), pages 187-198, 2010. Google Scholar
  78. Mary Southern and Kaustuv Chaudhuri. A two-level logic approach to reasoning about typed specification languages. In Venkatesh Raman and S. P. Suresh, editors, 34th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 29 of Leibniz International Proceedings in Informatics (LIPIcs), pages 557-569, New Delhi, India, 2014. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2014.557.
  79. Alwen Tiu. Model checking for π-calculus using proof search. In Martín Abadi and Luca de Alfaro, editors, Proceedings of CONCUR'05, volume 3653 of Lecture Notes in Computer Science, pages 36-50. Springer, 2005. Google Scholar
  80. Alwen Tiu and Dale Miller. A proof search specification of the π-calculus. In 3rd Workshop on the Foundations of Global Ubiquitous Computing, volume 138 of ENTCS, pages 79-101, 2005. URL: http://dx.doi.org/10.1016/j.entcs.2005.05.006.
  81. Alwen Tiu and Dale Miller. Proof search specifications of bisimulation and modal logics for the π-calculus. ACM Trans. on Computational Logic, 11(2), 2010. URL: http://dx.doi.org/10.1145/1656242.1656248.
  82. Alwen Tiu and Alberto Momigliano. Cut elimination for a logic with induction and co-induction. Journal of Applied Logic, 10(4):330-367, 2012. URL: http://dx.doi.org/10.1016/j.jal.2012.07.007.
  83. Christian Urban. Nominal reasoning techniques in Isabelle/HOL. Journal of Automated Reasoning, 40(4):327-356, 2008. Google Scholar
  84. Jean van Heijenoort. From Frege to Gödel: A Source Book in Mathematics, 1879-1931. Source books in the history of the sciences series. Harvard Univ. Press, Cambridge, MA, 3rd printing, 1997 edition, 1967. Google Scholar
  85. Myra VanInwegen. The Machine-Assisted Proof of Programming Language Properties. PhD thesis, University of Pennsylvania, may 1996. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact