{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:44Z","timestamp":1774837844729,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642140518","type":"print"},{"value":"9783642140525","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_17","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T10:23:14Z","timestamp":1278930194000},"page":"227-242","source":"Crossref","is-referenced-by-count":11,"title":["Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison"],"prefix":"10.1007","author":[{"given":"Amy","family":"Felty","sequence":"first","affiliation":[]},{"given":"Brigitte","family":"Pientka","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Aydemir","year":"2005","unstructured":"Aydemir, B., et al.: Mechanized metatheory for the masses: The POPLmark challenge. In: Hurd, J., Melham, T.F. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 50\u201365. Springer, Heidelberg (2005)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-14203-1_24","volume-title":"5th International Joint Conference on Automated Reasoning (IJCAR\u201910)","author":"D. Baelde","year":"2010","unstructured":"Baelde, D., Snow, Z., Miller, D.: Focused inductive theorem proving. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 278\u2013292. Springer, Heidelberg (2010)"},{"key":"17_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Dunfield, J., Pientka, B.: Case analysis of higher-order data. In: LFMTP\u201908. Electr. Notes in Theor. Comput. Sci, vol.\u00a0228, pp. 69\u201384 (2009)","DOI":"10.1016\/j.entcs.2008.12.117"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Felty, A.P., Momigliano, A.: Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax. CoRR, abs\/0811.4367 (2008)","DOI":"10.1016\/j.entcs.2007.09.019"},{"key":"17_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-71070-7_13","volume-title":"Automated Reasoning","author":"A. Gacek","year":"2008","unstructured":"Gacek, A.: The Abella interactive theorem prover (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 154\u2013161. Springer, Heidelberg (2008)"},{"issue":"1","key":"17_CR7","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\u00a040(1), 143\u2013184 (1993)","journal-title":"Journal of the ACM"},{"issue":"4-5","key":"17_CR8","doi-asserted-by":"publisher","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. Journal of Functional Programming\u00a017(4-5), 613\u2013673 (2007)","journal-title":"Journal of Functional Programming"},{"issue":"1","key":"17_CR9","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/504077.504080","volume":"3","author":"R.C. McDowell","year":"2002","unstructured":"McDowell, R.C., Miller, D.A.: Reasoning with higher-order abstract syntax in a logical framework. ACM Transactions on Computational Logic\u00a03(1), 80\u2013136 (2002)","journal-title":"ACM Transactions on Computational Logic"},{"key":"17_CR10","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: LFMTP\u201907. Electr. Notes Theor. Comput. Sci, vol.\u00a0196, pp. 85\u201393 (2008)","DOI":"10.1016\/j.entcs.2007.09.019"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"issue":"2","key":"17_CR12","doi-asserted-by":"publisher","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. Journal of Automated Reasoning\u00a034(2), 179\u2013207 (2005)","journal-title":"Journal of Automated Reasoning"},{"key":"17_CR13","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1145\/1328438.1328483","volume-title":"35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201908)","author":"B. Pientka","year":"2008","unstructured":"Pientka, B.: A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In: 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201908), pp. 371\u2013382. ACM Press, New York (2008)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-14203-1_2","volume-title":"5th International Joint Conference on Automated Reasoning (IJCAR\u201910).","author":"B. Pientka","year":"2010","unstructured":"Pientka, B., Dunfield, J.: Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 15\u201321. Springer, Heidelberg (2010)"},{"key":"17_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf \u2014 a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-78739-6_7","volume-title":"Programming Languages and Systems","author":"A.B. Poswolsky","year":"2008","unstructured":"Poswolsky, A.B., Sch\u00fcrmann, C.: Practical programming with higher-order encodings and dependent types. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 93\u2013107. Springer, Heidelberg (2008)"},{"key":"17_CR17","unstructured":"Sch\u00fcrmann, C.: Automating the Meta Theory of Deductive Systems. PhD thesis, Department of Computer Science, Carnegie Mellon University. CMU-CS-00-146 (2000)"},{"key":"17_CR18","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1109\/LICS.2008.44","volume-title":"23rd Annual Symposium on Logic in Computer Science (LICS)","author":"C. Sch\u00fcrmann","year":"2008","unstructured":"Sch\u00fcrmann, C., Sarnat, J.: Structural logical relations. In: 23rd Annual Symposium on Logic in Computer Science (LICS), pp. 69\u201380. IEEE Computer Society, Los Alamitos (2008)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:47:00Z","timestamp":1606168020000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}