{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:11:12Z","timestamp":1748751072218,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662488980"},{"type":"electronic","value":"9783662488997"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_28","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"402-417","source":"Crossref","is-referenced-by-count":2,"title":["A Contextual Logical Framework"],"prefix":"10.1007","author":[{"given":"Peter Brottveit","family":"Bock","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carsten","family":"Sch\u00fcrmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science (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. 5195, pp. 154\u2013161. Springer, Heidelberg (2008)"},{"key":"28_CR2","series-title":"London Mathematical Society Lecture Note Series","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/CBO9780511629150","volume-title":"Linear Logic: Its Syntax and Semantics","author":"J-Y Girard","year":"1995","unstructured":"Girard, J.-Y.: Linear Logic: Its Syntax and Semantics. London Mathematical Society Lecture Note Series, pp. 1\u201342. Cambridge University Press, New York (1995)"},{"issue":"1","key":"28_CR3","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. J. ACM (JACM) 40(1), 143\u2013184 (1993)","journal-title":"J. ACM (JACM)"},{"issue":"3","key":"28_CR4","doi-asserted-by":"publisher","first-page":"23","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. Logic (TOCL) 9(3), 23 (2008)","journal-title":"ACM Trans. Comput. Logic (TOCL)"},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Cervesato, I.: A linear logical framework. In: Clarke, E. (ed.) 11th Annual Symposium on Logic in Computer Science \u2013 LICS 1996, pp. 264\u2013275. IEEE Computer Society Press, New Brunswick, 27\u201330 July 1996. This work appeared as Preprint 1834 of the Department of Mathematics of Technical University of Darmstadt, Germany","DOI":"10.1109\/LICS.1996.561339"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science (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 - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"28_CR7","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 2008), pp. 371\u2013382. ACM (2008)","DOI":"10.1145\/1328438.1328483"},{"key":"28_CR8","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":"Automated Reasoning","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. 6173, pp. 15\u201321. Springer, Heidelberg (2010)"},{"issue":"2","key":"28_CR9","doi-asserted-by":"publisher","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."},{"key":"28_CR10","unstructured":"Poswolsky, A.: Functional Programming with Logical Frameworks: The Delphin Project. Ph.D. thesis, Yale University (2008)"},{"key":"28_CR11","unstructured":"Reed, J.: A hybrid logical framework. Ph.D. thesis, School of Computer Science, Carnegie Mellon University (2009)"},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework i: Judgments and properties. Technical report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University (2002)","DOI":"10.21236\/ADA418517"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T13:28:15Z","timestamp":1748698095000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}