{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T21:23:20Z","timestamp":1784150600378,"version":"3.55.0"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,7,5]],"date-time":"2015-07-05T00:00:00Z","timestamp":1436054400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2015,12]]},"DOI":"10.1007\/s10817-015-9327-3","type":"journal-article","created":{"date-parts":[[2015,7,4]],"date-time":"2015-07-04T12:45:18Z","timestamp":1436013918000},"page":"307-372","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations"],"prefix":"10.1007","volume":"55","author":[{"given":"Amy P.","family":"Felty","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alberto","family":"Momigliano","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Brigitte","family":"Pientka","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,7,5]]},"reference":[{"key":"9327_CR1","doi-asserted-by":"crossref","unstructured":"Accattoli, B.: Proof pearl: Abella formalization of \u03bb-calculus cube property. In: Second International Conference on Certified Programs and Proofs, Springer, LNCS, vol. 7679, pp. 173\u2013187 (2012)","DOI":"10.1007\/978-3-642-35308-6_15"},{"key":"9327_CR2","doi-asserted-by":"crossref","unstructured":"Ambler, S.J., Crole, R.L., Momigliano, A.: A definitional approach to primitive recursion over higher order abstract syntax. In: ACM Workshop on MEchanized Reasoning about Languages with varIable biNding, ACM Press, pp. 1\u201311 (2003)","DOI":"10.1145\/976571.976572"},{"key":"9327_CR3","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: Verified software toolchain. In: Programming Languages and Systems, Springer, LNCS, vol. 6602, pp. 1\u201317 (2011)","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"9327_CR4","doi-asserted-by":"crossref","unstructured":"Baelde, D.: On the expressivity of minimal generic quantification. In: Third International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2008, Elsevier, ENTCS, vol. 228, pp. 3\u201319 (2009)","DOI":"10.1016\/j.entcs.2008.12.113"},{"key":"9327_CR5","doi-asserted-by":"crossref","unstructured":"B\u00e9langer, O.S., Chaudhuri, K.: Automatically deriving schematic theorems for dynamic contexts. In: Ninth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, ACM Press, International Conference Proceedings Series, pp. 9:1\u20139:8 (2014)","DOI":"10.1145\/2631172.2631181"},{"key":"9327_CR6","doi-asserted-by":"crossref","unstructured":"de Bruijn, N.G.: A plea for weaker frameworks. In: Huet, G., Plotkin, G. (eds.), pp. 40\u201367. Cambridge University Press, Logical Frameworks (1991)","DOI":"10.1017\/CBO9780511569807.004"},{"key":"9327_CR7","doi-asserted-by":"crossref","unstructured":"Capretta, V., Felty, A.P.: Combining de Bruijn indices and higher-order abstract syntax in Coq. In: Types for Proofs and Programs, International Workshop, TYPES 2006, Springer, LNCS, vol. 4502, pp. 63\u201377 (2007)","DOI":"10.1007\/978-3-540-74464-1_5"},{"key":"9327_CR8","doi-asserted-by":"crossref","unstructured":"Cave, A., Pientka, B.: Programming with binders and indexed data-types. In: Thirty-Ninth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, pp. 413\u2013424 (2012)","DOI":"10.1145\/2103656.2103705"},{"key":"9327_CR9","doi-asserted-by":"crossref","unstructured":"Cave, A., Pientka, B.: First-class substitutions in contextual type theory. In: Eighth ACM SIGPLAN International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, ACM Press, pp. 15\u201324 (2013)","DOI":"10.1145\/2503887.2503889"},{"key":"9327_CR10","volume-title":"Mechanizing logical relation proofs using contextual types theory","author":"A Cave","year":"2014","unstructured":"Cave, A., Pientka, B.: Mechanizing logical relation proofs using contextual types theory. Tech. rep., School of Computer Science, McGill University (2014)"},{"key":"9327_CR11","doi-asserted-by":"crossref","unstructured":"Crary, K.: Explicit contexts in LF (extended abstract). In: Third International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2008, Elsevier, ENTCS, vol. 228, pp. 53\u201368 (2009)","DOI":"10.1016\/j.entcs.2008.12.116"},{"key":"9327_CR12","doi-asserted-by":"crossref","unstructured":"Dunfield, J., Pientka, B.: Case analysis of higher-order data. In: Third International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2008, Elsevier, ENTCS, vol. 228, pp. 69\u201384 (2009)","DOI":"10.1016\/j.entcs.2008.12.117"},{"key":"9327_CR13","doi-asserted-by":"crossref","unstructured":"Felty, A., Pientka, B.: Reasoning with higher-order abstract syntax and contexts: A comparison. In: First International Conference on Interactive Theorem Proving, Springer, LNCS, vol. 6172, pp. 227\u2013242 (2010)","DOI":"10.1007\/978-3-642-14052-5_17"},{"key":"9327_CR14","doi-asserted-by":"crossref","unstructured":"Felty, A.P.: Two-level meta-reasoning in Coq. In: Fifteenth International Conference on Theorem Proving in Higher-Order Logics, Springer, LNCS, vol. 2410, pp. 198\u2013213 (2002)","DOI":"10.1007\/3-540-45685-6_14"},{"key":"9327_CR15","doi-asserted-by":"crossref","unstructured":"Felty, A.P., Momigliano, A.: Reasoning with hypothetical judgments and open terms in Hybrid. In: Eleventh ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming, ACM Press, pp. 83\u201392 (2009)","DOI":"10.1145\/1599410.1599422"},{"issue":"1","key":"9327_CR16","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/s10817-010-9194-x","volume":"48","author":"AP Felty","year":"2012","unstructured":"Felty, A.P., Momigliano, A.: Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax. J. Autom. Reason. 48(1), 43\u2013105 (2012)","journal-title":"J. Autom. Reason."},{"key":"9327_CR17","unstructured":"Felty, A.P., Momigliano, A., Pientka, B.: The next 700 challenge problems for reasoning with higher-order abstract syntax representations: Part 1\u2014a common infrastructure for benchmarks. CoRR (2015). arXiv: 1503.06095"},{"key":"9327_CR18","doi-asserted-by":"crossref","unstructured":"Ferreira, F., Monnier, S., Pientka, B.: Compiling contextual objects: Bringing higher-order abstract syntax to programmers. In: Seventh ACM SIGPLAN Workshop on Programming Languages Meets Program Verification, ACM Press, pp. 13\u201324 (2013)","DOI":"10.1145\/2428116.2428121"},{"key":"9327_CR19","doi-asserted-by":"crossref","unstructured":"Gacek, A.: The Abella interactive theorem prover (system description), vol. 5195, pp. 154\u2013161 (2008)","DOI":"10.1007\/978-3-540-71070-7_13"},{"key":"9327_CR20","unstructured":"Gacek, A.: A framework for specifying, prototyping, and reasoning about computational systems. PhD thesis, University of Minnesota (2009)"},{"issue":"1","key":"9327_CR21","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1016\/j.ic.2010.09.004","volume":"209","author":"A Gacek","year":"2011","unstructured":"Gacek, A., Miller, D., Nadathur, G.: Nominal abstraction. Inf. Comput. 209(1), 48\u201373 (2011)","journal-title":"Inf. Comput."},{"issue":"2","key":"9327_CR22","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/s10817-011-9218-1","volume":"49","author":"A Gacek","year":"2012","unstructured":"Gacek, A., Miller, D., Nadathur, G.: A two-level logic approach to reasoning about computations. J. Autom. Reason. 49(2), 241\u2013273 (2012)","journal-title":"J. Autom. Reason."},{"key":"9327_CR23","doi-asserted-by":"crossref","unstructured":"Habli, N., Felty, A.P.: Translating higher-order specifications to Coq libraries supporting Hybrid proofs. In: Third International Workshop on Proof Exchange for Theorem Proving, EasyChair Proceedings in Computing, vol. 14, pp. 67\u201376 (2013)","DOI":"10.29007\/jqtz"},{"issue":"4-5","key":"9327_CR24","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1017\/S0956796807006430","volume":"17","author":"R Harper","year":"2007","unstructured":"Harper, R., Licata, D.R.: Mechanizing metatheory in a logical framework. J. Funct. Program. 17(4-5), 613\u2013673 (2007)","journal-title":"J. Funct. Program."},{"issue":"1","key":"9327_CR25","doi-asserted-by":"crossref","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. J. Assoc. Comput. Mach. 40(1), 143\u2013184 (1993)","journal-title":"J. Assoc. Comput. Mach."},{"issue":"7","key":"9327_CR26","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"1","key":"9327_CR27","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1145\/504077.504080","volume":"3","author":"RC McDowell","year":"2002","unstructured":"McDowell, R.C., Miller, D.A.: Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. Comput. Log. 3(1), 80\u2013136 (2002)","journal-title":"ACM Trans. Comput. Log."},{"key":"9327_CR28","doi-asserted-by":"crossref","unstructured":"Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press (2012)","DOI":"10.1017\/CBO9781139021326"},{"key":"9327_CR29","doi-asserted-by":"crossref","unstructured":"Momigliano, A.: A supposedly fun thing I may have to do again: A HOAS encoding of Howe\u2019s method. In: Seventh ACM SIGPLAN International Workshop on Logical Frameworks and Meta-Languages, Theory and Practice, ACM Press, pp. 33\u201342 (2012)","DOI":"10.1145\/2364406.2364411"},{"key":"9327_CR30","doi-asserted-by":"crossref","unstructured":"Momigliano, A., Ambler, S.J.: Multi-level meta-reasoning with higher order abstract syntax. In: Sixth International Conference on Foundations of Software Science and Computational Structures, Springer, LNCS, vol. 2620, pp. 375\u2013391 (2003)","DOI":"10.1007\/3-540-36576-1_24"},{"issue":"2","key":"9327_CR31","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1016\/S1571-0661(04)80506-1","volume":"70","author":"A Momigliano","year":"2002","unstructured":"Momigliano, A., Ambler, S., Crole, R.L.: A Hybrid encoding of Howe\u2019s method for establishing congruence of bisimilarity. Electr. Notes Theor. Comput. Sci. 70(2), 60\u201375 (2002)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9327_CR32","doi-asserted-by":"crossref","unstructured":"Momigliano, A., Martin, A.J., Felty, A.P.: Two-level Hybrid: A system for reasoning using higher-order abstract syntax. In: Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2007, Elsevier, ENTCS, vol. 196, pp. 85\u201393 (2008)","DOI":"10.1016\/j.entcs.2007.09.019"},{"issue":"3","key":"9327_CR33","doi-asserted-by":"crossref","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 Trans. Comput. Log. 9(3), 1\u201349 (2008)","journal-title":"ACM Trans. Comput. Log."},{"key":"9327_CR34","unstructured":"Pfenning, F.: Computation and deduction, http:\/\/www.cs.cmu.edu\/~fp\/courses\/comp-ded\/handouts\/cd.pdf , accessed 14 October 2014 (2001)"},{"issue":"2","key":"9327_CR35","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/s10817-005-6534-3","volume":"34","author":"B Pientka","year":"2005","unstructured":"Pientka, B.: Verifying termination and reduction properties about higher-order logic programs. J. Autom. Reason. 34(2), 179\u2013207 (2005)","journal-title":"J. Autom. Reason."},{"key":"9327_CR36","doi-asserted-by":"crossref","unstructured":"Pientka, B.: A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In: Thirty-Fifth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, pp. 371\u2013382 (2008)","DOI":"10.1145\/1328438.1328483"},{"key":"9327_CR37","doi-asserted-by":"crossref","unstructured":"Pientka, B.: Programming inductive proofs: A new approach based on contextual types. In: Verification, Induction, Termination Analysis: Festschrift for Christoph Walther, Springer, LNCS, vol. 6463, pp. 1\u201316 (2010)","DOI":"10.1007\/978-3-642-17172-7_1"},{"key":"9327_CR38","unstructured":"Pientka, B., Abel, A.: Structural recursion over contextual objects. In: Thirteenth International Conference on Typed Lambda Calculi and Applications, Leibniz International Proceedings in Informatics (LIPIcs) of Schloss Dagstuhl (forthcoming) (2015)"},{"key":"9327_CR39","doi-asserted-by":"crossref","unstructured":"Pientka, B., Dunfield, J.: Programming with proofs and explicit contexts. In: Tenth ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, ACM Press, pp. 163\u2013173 (2008)","DOI":"10.1145\/1389449.1389469"},{"key":"9327_CR40","doi-asserted-by":"crossref","unstructured":"Pientka, B., Dunfield, J.: Beluga: A framework for programming and reasoning with deductive systems (system description). In: Fifth International Joint Conference on Automated Reasoning, Springer, LNCS, vol. 6173, pp. 15\u201321 (2010)","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"9327_CR41","doi-asserted-by":"crossref","unstructured":"Rohwedder, E., Pfenning, F.: Mode and termination checking for higher-order logic programs. In: Programming Languages and Systems: Sixth European Symposium on Programming, Springer, LNCS, vol. 1058, pp. 296\u2013310 (1996)","DOI":"10.1007\/3-540-61055-3_44"},{"key":"9327_CR42","doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann, C.: The Twelf proof assistant. In: Twenty-Second International Conference on Theorem Proving in Higher Order Logics, Springer, LNCS, vol. 5674, pp. 79\u201383 (2009)","DOI":"10.1007\/978-3-642-03359-9_7"},{"key":"9327_CR43","doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann, C., Pfenning, F.: Automated theorem proving in a simple meta-logic for LF. In: Fifteenth International Conference on Automated Deduction, Springer, LNCS, vol. 1421, pp. 286\u2013300 (1998)","DOI":"10.1007\/BFb0054266"},{"key":"9327_CR44","doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann, C., Pfenning, F.: A coverage checking algorithm for LF. In: Sixteenth International Conference on Theorem Proving in Higher Order Logics, Springer, LNCS, vol. 2758, pp. 120\u2013135 (2003)","DOI":"10.1007\/10930755_8"},{"issue":"4","key":"9327_CR45","doi-asserted-by":"crossref","first-page":"330","DOI":"10.1016\/j.jal.2012.07.007","volume":"10","author":"A Tiu","year":"2012","unstructured":"Tiu, A., Momigliano, A.: Cut elimination for a logic with induction and co-induction. J. Appl. Log. 10(4), 330\u2013367 (2012)","journal-title":"J. Appl. Log."},{"key":"9327_CR46","doi-asserted-by":"crossref","unstructured":"Wang, Y., Nadathur, G.: Towards extracting explicit proofs from totality checking in Twelf. In: Eighth ACM SIGPLAN International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, ACM Press, pp. 55\u201366 (2013)","DOI":"10.1145\/2503887.2503893"},{"key":"9327_CR47","doi-asserted-by":"crossref","unstructured":"Wang, Y., Chaudhuri, K., Gacek, A., Nadathur, G.: Reasoning about higher-order relational specifications. In: Fifteenth International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, ACM Press, pp. 157\u2013168 (2013)","DOI":"10.1145\/2505879.2505889"},{"key":"9327_CR48","doi-asserted-by":"crossref","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. In: Thirty-Ninth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, pp. 427\u2013440 (2012)","DOI":"10.1145\/2103656.2103709"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9327-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9327-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9327-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T00:59:33Z","timestamp":1748480373000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9327-3"}},"subtitle":["Part 2\u2014A Survey"],"short-title":[],"issued":{"date-parts":[[2015,7,5]]},"references-count":48,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,12]]}},"alternative-id":["9327"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9327-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,7,5]]}}}