Harpoon: mechanizing metatheory interactively. (English) Zbl 1540.68266
Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 636-648 (2021).
Summary: Beluga is a proof checker that provides sophisticated infrastructure for implementing formal systems with the logical framework LF and proving metatheoretic properties as total, recursive functions transforming LF derivations. In this paper, we describe Harpoon, an interactive proof engine built on top of Beluga. It allows users to develop proofs interactively using a small, fixed set of high-level actions that safely transform a subgoal. A sequence of actions elaborates into a (partial) proof script that serves as an intermediate representation describing an assertion-level proof. Last, a proof script translates into a Beluga program which can be type-checked independently. Harpoon is available on GitHub. We have used Harpoon to replay a wide array of examples covering all features supported by Beluga. In particular, we have used it for normalization proofs, including the recently proposed POPLMark reloaded challenge.
For the entire collection see [Zbl 1475.68026].
For the entire collection see [Zbl 1475.68026].
MSC:
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | Abel, A., Allais, G., Hameer, A., Pientka, B., Momigliano, A., Schäfer, S., Stark, K.: POPLMark Reloaded: Mechanizing Proofs by Logical Relations. J. Funct. Program. 29, e19 (2019). doi:10.1017/S0956796819000170 · Zbl 1442.68257 |
| [2] | Abel, A., Chang, B.Y.E., Pfenning, F.: Human-readable machine-verifiable proofs for teaching constructive logic. In: Egly, U., Fiedler, A., Horacek, H., Schmitt, S. (eds.) Proceedings of the Workshop on Proof Transformation and Presentation and Proof Complexities (PTP’01). pp. 33-48. Siena, Italy (2001), http://www2.tcs.ifi.lmu.de/ abel/ptp01.pdf |
| [3] | Boespflug, M., Pientka, B.: Multi-level contextual modal type theory. In: Nadathur, G., Geuvers, H. (eds.) 6th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP’11). Electronic Proceedings in Theoretical Computer Science (EPTCS), vol. 71, pp. 29-43 (2011) |
| [4] | Cave, A., Pientka, B.: Programming with binders and indexed data-types. In: 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’12). pp. 413-424. ACM Press (2012) · Zbl 1321.68141 |
| [5] | Cave, A., Pientka, B.: First-class substitutions in contextual type theory. In: 8th ACM SIGPLAN International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP’13). pp. 15-24. ACM Press (2013) |
| [6] | Cave, A.; Pientka, B., Mechanizing Proofs with Logical Relations - Kripke-style, Mathematical Structures in Computer Science, 28, 9, 1606-1638 (2018) · Zbl 1400.68193 · doi:10.1017/S0960129518000154 |
| [7] | Delahaye, D.: A tactic language for the system Coq. In: Parigot, M., Voronkov, A. (eds.) 7th International Conference on Logic for Programming and Automated Reasoning (LPAR’00). Lecture Notes in Computer Science, vol. 1955, pp. 85-95. Springer (2000). doi:10.1007/3-540-44404-1_7 · Zbl 0988.68584 |
| [8] | Errington, J.: Mechanizing metatheory interactively. Master’s thesis, McGill University (2020) · Zbl 1540.68266 |
| [9] | Felty, AF; Momigliano, A.; Pientka, B., Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions, Math. Struct. in Comp. Science, 28, 9, 1507-1540 (2018) · Zbl 1400.68194 · doi:10.1017/S0960129517000093 |
| [10] | Felty, A.P., Momigliano, A., Pientka, B.: The next 700 challenge problems for reasoning with higher-order abstract syntax representations: Part 2 - a survey. Journal of Automated Reasoning 55(4), 307-372 (2015). doi:10.1007/s10817-015-9327-3 · Zbl 1357.68198 |
| [11] | Gacek, A.: The Abella interactive theorem prover (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) 4th International Joint Conference on Automated Reasoning. Lecture Notes in Artificial Intelligence, vol. 5195, pp. 154-161. Springer (2008) · Zbl 1165.68457 |
| [12] | Gacek, A., Miller, D., Nadathur, G.: Combining generic judgments with recursive definitions. In: Pfenning, F. (ed.) 23rd Symposium on Logic in Computer Science. IEEE Computer Society Press (2008) |
| [13] | Harper, R.; Honsell, F.; Plotkin, G., A framework for defining logics, Journal of the ACM, 40, 1, 143-184 (1993) · Zbl 0778.03004 · doi:10.1145/138027.138060 |
| [14] | Heilala, S., Pientka, B.: Bidirectional decision procedures for the intuitionistic propositional modal logic is4. In: Pfenning, F. (ed.) 21st International Conference on Automated Deduction (CADE 2007). pp. 116-131. Lecture Notes in Computer Science (LNCS 4603), Springer (2007) · Zbl 1213.03029 |
| [15] | Huang, X.: Reconstruction proofs at the assertion level. In: Bundy, A. (ed.) Proceedings of the 12th International Conference on Automated Deduction (CADE-12). Lecture Notes in Computer Science, vol. 814, pp. 738-752. Springer (1994). doi:10.1007/3-540-58156-1_53 · Zbl 1433.68551 |
| [16] | Jacob-Rao, R., Pientka, B., Thibodeau, D.: Index-stratified types. In: Kirchner, H. (ed.) 3rd International Conference on Formal Structures for Computation and Deduction (FSCD’18). pp. 19:1-19:17. LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (January 2018) · Zbl 1462.68021 |
| [17] | Kaiser, J., Ziliani, B., Krebbers, R., Régis-Gianas, Y., Dreyer, D.: Mtac2: typed tactics for backward reasoning in coq. Proc. ACM Program. Lang. 2(ICFP), 78:1-78:31 (2018). doi:10.1145/3236773 |
| [18] | Lee, D.K., Crary, K., Harper, R.: Towards a mechanized metatheory of Standard ML. In: 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’07). pp. 173-184. ACM Press (2007) · Zbl 1295.68088 |
| [19] | Nanevski, A.; Pfenning, F.; Pientka, B., Contextual modal type theory, ACM Transactions on Computational Logic, 9, 3, 1-49 (2008) · Zbl 1367.03060 · doi:10.1145/1352582.1352591 |
| [20] | Pfenning, F., Schürmann, C.: System description: Twelf — A Meta-Logical Framework for Deductive Systems. In: Ganzinger, H. (ed.) 16th International Conference on Automated Deduction (CADE-16). pp. 202-206. Lecture Notes in Artificial Intelligence (LNAI 1632), Springer (1999) |
| [21] | Pientka, B.: A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In: 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08). pp. 371-382. ACM Press (2008) · Zbl 1295.68068 |
| [22] | Pientka, B.: Programming inductive proofs: a new approach based on contextual types. In: Siegler, S., Wasser, N. (eds.) Verification, Induction, Termination Analysis - Festschrift for Christoph Walther on the Occasion of his 60th Birthday. pp. 1-16. Lecture Notes in Computer Science (LNCS 6463), Springer (2010) · Zbl 1309.68051 |
| [23] | Pientka, B.: An insider’s look at LF type reconstruction: Everything you (n)ever wanted to know. Journal of Functional Programming 1(1-37) (2013) · Zbl 1262.68030 |
| [24] | Pientka, B., Abel, A.: Structural recursion over contextual objects. In: Altenkirch, T. (ed.) 13th International Conference on Typed Lambda Calculi and Applications (TLCA’15). pp. 273-287. Leibniz International Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl (2015) · Zbl 1367.68073 |
| [25] | Pientka, B., Cave, A.: Inductive Beluga: Programming Proofs (System Description). In: Felty, A.P., Middeldorp, A. (eds.) 25th International Conference on Automated Deduction (CADE-25). pp. 272-281. Lecture Notes in Computer Science (LNCS 9195), Springer (2015) · Zbl 1465.68294 |
| [26] | Pientka, B., Dunfield, J.: Programming with proofs and explicit contexts. In: ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP’08). pp. 163-173. ACM Press (2008) |
| [27] | Schürmann, C.: Automating the Meta Theory of Deductive Systems. Ph.D. thesis, Department of Computer Science, Carnegie Mellon University (2000), CMU-CS-00-146 |
| [28] | Schürmann, C., Pfenning, F.: Automated theorem proving in a simple meta-logic for LF. In: Kirchner, C., Kirchner, H. (eds.) Proceedings of the 15th International Conference on Automated Deduction (CADE-15). pp. 286-300. Springer-Verlag Lecture Notes in Computer Science (LNCS) 1421, Lindau, Germany (Jul 1998) · Zbl 0924.03024 |
| [29] | Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: A monad for typed tactic programming in Coq. Journal of Functional Programming 25 (2015) · Zbl 1420.68189 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
