{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T09:38:54Z","timestamp":1743154734285,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:sc>Beluga<\/jats:sc>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<jats:sc>Harpoon<\/jats:sc>, an interactive proof engine built on top of<jats:sc>Beluga<\/jats:sc>. It allows users to develop proofs interactively using a small, fixed set of high-level<jats:italic>actions<\/jats:italic>that safely transform a subgoal. A sequence of actions elaborates into a (partial)<jats:italic>proof script<\/jats:italic>that serves as an intermediate representation describing an assertion-level proof. Last, a proof script translates into a<jats:sc>Beluga<\/jats:sc>program which can be type-checked independently.<jats:sc>Harpoon<\/jats:sc>is available on GitHub. We have used<jats:sc>Harpoon<\/jats:sc>to replay a wide array of examples covering all features supported by<jats:sc>Beluga<\/jats:sc>. In particular, we have used it for normalization proofs, including the recently proposed POPLMark reloaded challenge.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_38","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"636-648","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Harpoon: Mechanizing Metatheory Interactively"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4307-7505","authenticated-orcid":false,"given":"Jacob","family":"Errington","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6338-2155","authenticated-orcid":false,"given":"Junyoung","family":"Jang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2549-4276","authenticated-orcid":false,"given":"Brigitte","family":"Pientka","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"38_CR1","doi-asserted-by":"publisher","unstructured":"Abel, A., Allais, G., Hameer, A., Pientka, B., Momigliano, A., Sch\u00e4fer, S., Stark, K.: POPLMark Reloaded: Mechanizing Proofs by Logical Relations. J. Funct. Program. 29, e19 (2019). https:\/\/doi.org\/10.1017\/S0956796819000170","DOI":"10.1017\/S0956796819000170"},{"key":"38_CR2","unstructured":"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\u201901). pp. 33\u201348. Siena, Italy (2001), http:\/\/www2.tcs.ifi.lmu.de\/~abel\/ptp01.pdf"},{"key":"38_CR3","doi-asserted-by":"crossref","unstructured":"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\u201911). Electronic Proceedings in Theoretical Computer Science (EPTCS), vol. 71, pp. 29\u201343 (2011)","DOI":"10.4204\/EPTCS.71.3"},{"key":"38_CR4","doi-asserted-by":"crossref","unstructured":"Cave, A., Pientka, B.: Programming with binders and indexed data-types. In: 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201912). pp. 413\u2013424. ACM Press (2012)","DOI":"10.1145\/2103656.2103705"},{"key":"38_CR5","doi-asserted-by":"crossref","unstructured":"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\u201913). pp. 15\u201324. ACM Press (2013)","DOI":"10.1145\/2503887.2503889"},{"issue":"9","key":"38_CR6","doi-asserted-by":"publisher","first-page":"1606","DOI":"10.1017\/S0960129518000154","volume":"28","author":"A Cave","year":"2018","unstructured":"Cave, A., Pientka, B.: Mechanizing Proofs with Logical Relations - Kripke-style. Mathematical Structures in Computer Science 28(9), 1606\u20131638 (2018). https:\/\/doi.org\/10.1017\/S0960129518000154","journal-title":"Mathematical Structures in Computer Science"},{"key":"38_CR7","doi-asserted-by":"publisher","unstructured":"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\u201900). Lecture Notes in Computer Science, vol. 1955, pp. 85\u201395. Springer (2000). https:\/\/doi.org\/10.1007\/3-540-44404-1_7","DOI":"10.1007\/3-540-44404-1_7"},{"key":"38_CR8","doi-asserted-by":"crossref","unstructured":"Errington, J.: Mechanizing metatheory interactively. Master\u2019s thesis, McGill University (2020)","DOI":"10.1007\/978-3-030-79876-5_38"},{"issue":"9","key":"38_CR9","doi-asserted-by":"publisher","first-page":"1507","DOI":"10.1017\/S0960129517000093","volume":"28","author":"AF Felty","year":"2018","unstructured":"Felty, A.F., Momigliano, A., Pientka, B.: Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions. Math. Struct. in Comp. Science 28(9), 1507\u20131540 (2018). https:\/\/doi.org\/10.1017\/S0960129517000093","journal-title":"Math. Struct. in Comp. Science"},{"key":"38_CR10","doi-asserted-by":"publisher","unstructured":"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\u2013372 (2015). https:\/\/doi.org\/10.1007\/s10817-015-9327-3","DOI":"10.1007\/s10817-015-9327-3"},{"key":"38_CR11","doi-asserted-by":"crossref","unstructured":"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\u2013161. Springer (2008)","DOI":"10.1007\/978-3-540-71070-7_13"},{"key":"38_CR12","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1109\/LICS.2008.33"},{"issue":"1","key":"38_CR13","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the ACM 40(1), 143\u2013184 (1993)","journal-title":"Journal of the ACM"},{"key":"38_CR14","doi-asserted-by":"crossref","unstructured":"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\u2013131. Lecture Notes in Computer Science (LNCS 4603), Springer (2007)","DOI":"10.1007\/978-3-540-73595-3_9"},{"key":"38_CR15","doi-asserted-by":"publisher","unstructured":"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\u2013752. Springer (1994). https:\/\/doi.org\/10.1007\/3-540-58156-1_53","DOI":"10.1007\/3-540-58156-1_53"},{"key":"38_CR16","unstructured":"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\u201918). pp. 19:1\u201319:17. LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (January 2018)"},{"key":"38_CR17","doi-asserted-by":"publisher","unstructured":"Kaiser, J., Ziliani, B., Krebbers, R., R\u00e9gis-Gianas, Y., Dreyer, D.: Mtac2: typed tactics for backward reasoning in coq. Proc. ACM Program. Lang. 2(ICFP), 78:1\u201378:31 (2018). https:\/\/doi.org\/10.1145\/3236773","DOI":"10.1145\/3236773"},{"key":"38_CR18","doi-asserted-by":"crossref","unstructured":"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\u201907). pp. 173\u2013184. ACM Press (2007)","DOI":"10.1145\/1190216.1190245"},{"issue":"3","key":"38_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1352582.1352591","volume":"9","author":"A Nanevski","year":"2008","unstructured":"Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Transactions on Computational Logic 9(3), 1\u201349 (2008)","journal-title":"ACM Transactions on Computational Logic"},{"key":"38_CR20","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf \u2014 A Meta-Logical Framework for Deductive Systems. In: Ganzinger, H. (ed.) 16th International Conference on Automated Deduction (CADE-16). pp. 202\u2013206. Lecture Notes in Artificial Intelligence (LNAI 1632), Springer (1999)","DOI":"10.1007\/3-540-48660-7_14"},{"key":"38_CR21","doi-asserted-by":"crossref","unstructured":"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\u201908). pp. 371\u2013382. ACM Press (2008)","DOI":"10.1145\/1328438.1328483"},{"key":"38_CR22","doi-asserted-by":"crossref","unstructured":"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\u201316. Lecture Notes in Computer Science (LNCS 6463), Springer (2010)","DOI":"10.1007\/978-3-642-17172-7_1"},{"key":"38_CR23","doi-asserted-by":"crossref","unstructured":"Pientka, B.: An insider\u2019s look at LF type reconstruction: Everything you (n)ever wanted to know. Journal of Functional Programming 1(1\u201337) (2013)","DOI":"10.1017\/S0956796812000408"},{"key":"38_CR24","unstructured":"Pientka, B., Abel, A.: Structural recursion over contextual objects. In: Altenkirch, T. (ed.) 13th International Conference on Typed Lambda Calculi and Applications (TLCA\u201915). pp. 273\u2013287. Leibniz International Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl (2015)"},{"key":"38_CR25","doi-asserted-by":"crossref","unstructured":"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\u2013281. Lecture Notes in Computer Science (LNCS 9195), Springer (2015)","DOI":"10.1007\/978-3-319-21401-6_18"},{"key":"38_CR26","doi-asserted-by":"crossref","unstructured":"Pientka, B., Dunfield, J.: Programming with proofs and explicit contexts. In: ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP\u201908). pp. 163\u2013173. ACM Press (2008)","DOI":"10.1145\/1389449.1389469"},{"key":"38_CR27","unstructured":"Sch\u00fcrmann, C.: Automating the Meta Theory of Deductive Systems. Ph.D. thesis, Department of Computer Science, Carnegie Mellon University (2000), CMU-CS-00-146"},{"key":"38_CR28","doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann, 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\u2013300. Springer-Verlag Lecture Notes in Computer Science (LNCS) 1421, Lindau, Germany (Jul 1998)","DOI":"10.1007\/BFb0054266"},{"key":"38_CR29","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1017\/S0956796815000118"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T05:32:12Z","timestamp":1672723932000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_38"}},"subtitle":["(System Description)"],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"76","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}