{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:56Z","timestamp":1761611276744},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2011,2,23]],"date-time":"2011-02-23T00:00:00Z","timestamp":1298419200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1007\/s10817-011-9218-1","type":"journal-article","created":{"date-parts":[[2011,2,22]],"date-time":"2011-02-22T05:50:58Z","timestamp":1298353858000},"page":"241-273","source":"Crossref","is-referenced-by-count":33,"title":["A Two-Level Logic Approach to Reasoning About Computations"],"prefix":"10.1007","volume":"49","author":[{"given":"Andrew","family":"Gacek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dale","family":"Miller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gopalan","family":"Nadathur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,2,23]]},"reference":[{"key":"9218_CR1","doi-asserted-by":"crossref","unstructured":"Aydemir, B., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: 35th ACM Symp. on Principles of Programming Languages, pp. 3\u201315. ACM (2008)","DOI":"10.1145\/1328438.1328443"},{"key":"9218_CR2","doi-asserted-by":"crossref","unstructured":"Aydemir, B.E., Bohannon, A., Fairbairn, M., Foster, J.N., Pierce, B.C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: the POPLmark challenge. In: Theorem Proving in Higher Order Logics: 18th International Conference, number 3603 in LNCS, pp. 50\u201365. Springer (2005)","DOI":"10.1007\/11541868_4"},{"key":"9218_CR3","unstructured":"Baelde, D.: A Linear Approach to the Proof-Theory of Least and Greatest Fixed Points. PhD thesis, Ecole Polytechnique (2008)"},{"key":"9218_CR4","doi-asserted-by":"crossref","unstructured":"Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning, F. (ed.) 21th Conference on Automated Deduction (CADE), number 4603 in LNAI, pp. 391\u2013397. Springer (2007)","DOI":"10.1007\/978-3-540-73595-3_28"},{"key":"9218_CR5","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9218_CR6","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5, 56\u201368 (1940)","journal-title":"J. Symb. Logic"},{"key":"9218_CR7","doi-asserted-by":"crossref","unstructured":"Coquand, T., Paulin, C.: Inductively defined types. In: Conference on Computer Logic. LNCS, vol. 417, pp. 50\u201366. Springer (1988)","DOI":"10.1007\/3-540-52335-9_47"},{"key":"9218_CR8","doi-asserted-by":"crossref","unstructured":"Despeyroux, J., Felty, A., Hirschowitz, A.: Higher-order abstract syntax in Coq. In: Second International Conference on Typed Lambda Calculi and Applications, pp. 124\u2013138 (1995)","DOI":"10.1007\/BFb0014049"},{"key":"9218_CR9","doi-asserted-by":"crossref","unstructured":"Felty, A., Momigliano, A.: Reasoning with hypothetical judgments and open terms in Hybrid. In: ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), pp. 83\u201392 (2009)","DOI":"10.1145\/1599410.1599422"},{"key":"9218_CR10","author":"A Felty","year":"2010","unstructured":"Felty, A., Momigliano, A.: Hybrid: a definitional two-level approach to reasoning with higher-order abstract syntax. J. Autom. Reason. (2010). doi: 10.1007\/s10817-010-9194-x","journal-title":"J. Autom. Reason."},{"key":"9218_CR11","unstructured":"Gacek, A.: The Abella interactive theorem prover (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Fourth International Joint Conference on Automated Reasoning. LNCS, vol. 5195, pp. 154\u2013161. Springer (2008). URL http:\/\/arxiv.org\/abs\/0803.2305"},{"key":"9218_CR12","unstructured":"Gacek, A.: The Abella System and Homepage. http:\/\/abella.cs.umn.edu\/ (2009)"},{"key":"9218_CR13","unstructured":"Gacek, A.: A Framework for Specifying, Prototyping, and Reasoning About Computational Systems. PhD thesis, University of Minnesota (2009)"},{"key":"9218_CR14","unstructured":"Gacek, A., Holte, S., Nadathur, G., Qi, X., Snow, Z.: The Teyjus System\u2013Version 2, March 2008. Available from http:\/\/teyjus.cs.umn.edu\/"},{"issue":"1","key":"9218_CR15","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":"1","key":"9218_CR16","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. ACM 40(1), 143\u2013184 (1993)","journal-title":"J. ACM"},{"key":"9218_CR17","doi-asserted-by":"crossref","unstructured":"Kahn, G.: Natural semantics. In: Proceedings of the Symposium on Theoretical Aspects of Computer Science. LNCS, vol. 247, pp. 22\u201339. Springer (1987)","DOI":"10.1007\/BFb0039592"},{"issue":"5","key":"9218_CR18","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","volume":"6","author":"PJ Landin","year":"1964","unstructured":"Landin, P.J.: The mechanical evaluation of expressions. Comput. J. 6(5), 308\u2013320 (1964)","journal-title":"Comput. J."},{"key":"9218_CR19","doi-asserted-by":"crossref","unstructured":"Licata, D.R., Zeilberger, N., Harper, R.: Focusing on binding and computation. In: Pfenning, F. (ed.) 23th Symp. on Logic in Computer Science, pp. 241\u2013252. IEEE Computer Society Press (2008)","DOI":"10.1109\/LICS.2008.48"},{"key":"9218_CR20","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/S0304-3975(99)00171-1","volume":"232","author":"R McDowell","year":"2000","unstructured":"McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theor. Comp. Sci. 232, 91\u2013119 (2000)","journal-title":"Theor. Comp. Sci."},{"issue":"1","key":"9218_CR21","doi-asserted-by":"crossref","first-page":"80","DOI":"10.1145\/504077.504080","volume":"3","author":"R McDowell","year":"2002","unstructured":"McDowell, R., Miller, D. 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."},{"issue":"4","key":"9218_CR22","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","volume":"14","author":"D Miller","year":"1992","unstructured":"Miller, D.: Unification under a mixed prefix. J. Symb. Comput. 14(4), 321\u2013358 (1992)","journal-title":"J. Symb. Comput."},{"key":"9218_CR23","doi-asserted-by":"crossref","unstructured":"Miller, D.: Abstract syntax for variable binders: an overview. In: Lloyd, J., et al. (eds.) Computational Logic\u2014CL 2000, number 1861 in LNAI, pp. 239\u2013253. Springer (2000)","DOI":"10.1007\/3-540-44957-4_16"},{"key":"9218_CR24","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D Miller","year":"1991","unstructured":"Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Logic 51, 125\u2013157 (1991)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"4","key":"9218_CR25","doi-asserted-by":"crossref","first-page":"749","DOI":"10.1145\/1094622.1094628","volume":"6","author":"D Miller","year":"2005","unstructured":"Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. Comput. Log. 6(4), 749\u2013783 (2005)","journal-title":"ACM Trans. Comput. Log."},{"key":"9218_CR26","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1017\/S0960129500001407","volume":"2","author":"R Milner","year":"1992","unstructured":"Milner, R.: Functions as processes. Math. Struct. Comput. Sci. 2, 119\u2013141 (1992)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9218_CR27","unstructured":"Nadathur, G., Miller, D.: An overview of \u03bbProlog. In: Fifth International Logic Programming Conference, Seattle, pp. 810\u2013827. MIT Press (1988)"},{"key":"9218_CR28","doi-asserted-by":"crossref","unstructured":"Nadathur, G., Mitchell, D.J.: System description: Teyjus\u2014a compiler and abstract machine based implementation of \u03bbProlog. In: Ganzinger, H. (ed.) 16th Conference on Automated Deduction (CADE), number 1632 in LNAI, Trento, pp. 287\u2013291. Springer (1999)","DOI":"10.1007\/3-540-48660-7_25"},{"key":"9218_CR29","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer (2002). LNCS Tutorial 2283","DOI":"10.1007\/3-540-45949-9"},{"key":"9218_CR30","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf\u2014a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) 16th Conference on Automated Deduction (CADE), number 1632 in LNAI, Trento, pp. 202\u2013206. Springer (1999)","DOI":"10.1007\/3-540-48660-7_14"},{"key":"9218_CR31","doi-asserted-by":"crossref","unstructured":"Pientka, B.: A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In: 35th Annual ACM Symposium on Principles of Programming Languages (POPL\u201908), pp. 371\u2013382. ACM (2008)","DOI":"10.1145\/1328438.1328483"},{"issue":"2","key":"9218_CR32","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"AM Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165\u2013193 (2003)","journal-title":"Inf. Comput."},{"issue":"1","key":"9218_CR33","first-page":"125","volume":"1","author":"G Plotkin","year":"1976","unstructured":"Plotkin, G.: Call-by-name, call-by-value and the \u03bb-calculus. Theor. Comp. Sci. 1(1), 125\u2013159 (1976)","journal-title":"Theor. Comp. Sci."},{"key":"9218_CR34","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"G Plotkin","year":"1977","unstructured":"Plotkin, G.: LCF as a programming language. Theor. Comp. Sci. 5, 223\u2013255 (1977)","journal-title":"Theor. Comp. Sci."},{"key":"9218_CR35","unstructured":"Plotkin, G.: A Structural Approach to Operational Semantics. DAIMI FN-19, Aarhus University, Aarhus, Denmark (1981)"},{"key":"9218_CR36","doi-asserted-by":"crossref","unstructured":"Poswolsky, A., Sch\u00fcrmann, C.: System description: Delphin\u2014a functional programming language for deductive systems. In: Abel, A., Urban, C. (eds.) International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008), vol. 228, pp. 113\u2013120 (2008)","DOI":"10.1016\/j.entcs.2008.12.120"},{"key":"9218_CR37","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Definitional interpreters for higher order programming languages. In: ACM Conference Proceedings, pp. 717\u2013740. ACM (1972)","DOI":"10.1145\/800194.805852"},{"issue":"1","key":"9218_CR38","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1006\/inco.1994.1042","volume":"111","author":"D Sangiorgi","year":"1994","unstructured":"Sangiorgi, D.: The lazy lambda calculus in a concurrency scenario. Inf. Comput. 111(1), 120\u2013153 (1994)","journal-title":"Inf. Comput."},{"key":"9218_CR39","unstructured":"Sch\u00fcrmann, C.: Automating the Meta Theory of Deductive Systems. PhD thesis, Carnegie Mellon University (2000). CMU-CS-00-146"},{"key":"9218_CR40","unstructured":"Smorynski, C.: Modal logic and self-reference. In: Gabbay, D., Guenther, F. (eds.) Handbook of Philosophical Logic, vol. 11, 2nd edn., pp. 1\u201354. Kluwer Academic (2004)"},{"key":"9218_CR41","unstructured":"Tiu, A.: A Logical Framework for Reasoning about Logical Specifications. PhD thesis, Pennsylvania State University (2004)"},{"key":"9218_CR42","unstructured":"Tiu, A.: A logic for reasoning about generic judgments. In: Momigliano, A., Pientka, B. (eds.) Int. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP\u201906) (2006)"},{"key":"9218_CR43","unstructured":"Tiu, A., Momigliano, A.: Induction and Co-Induction in Sequent Calculus. Available from http:\/\/arxiv.org\/abs\/0812.4727 (2009)"},{"issue":"4","key":"9218_CR44","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/s10817-008-9097-2","volume":"40","author":"C Urban","year":"2008","unstructured":"Urban, C.: Nominal reasoning techniques in Isabelle\/HOL. J. Autom. Reason. 40(4), 327\u2013356 (2008)","journal-title":"J. Autom. Reason."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9218-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-011-9218-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-011-9218-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T18:48:50Z","timestamp":1560019730000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-011-9218-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,2,23]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["9218"],"URL":"https:\/\/doi.org\/10.1007\/s10817-011-9218-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,2,23]]}}}