{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:38:10Z","timestamp":1725557890749},"publisher-location":"Berlin, Heidelberg","reference-count":68,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642143083"},{"type":"electronic","value":"9783642143090"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14309-0_12","type":"book-chapter","created":{"date-parts":[[2010,6,23]],"date-time":"2010-06-23T13:09:58Z","timestamp":1277298598000},"page":"254-270","source":"Crossref","is-referenced-by-count":1,"title":["Proof-Theoretic and Higher-Order Extensions of Logic Programming"],"prefix":"10.1007","author":[{"given":"Alberto","family":"Momigliano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mario","family":"Ornaghi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"Alpuente, M., Sessa, M.I. (eds.): 1995 Joint Conference on Declarative Programming, GULP-PRODE 1995, Marina di Vietri, Italy (1995)"},{"issue":"3","key":"12_CR2","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J.-M. Andreoli","year":"1992","unstructured":"Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. J. Log. Comput.\u00a02(3), 297\u2013347 (1992)","journal-title":"J. Log. Comput."},{"key":"12_CR3","first-page":"295","volume-title":"Proceedings of the International Logic Programming Symposium","author":"J.-M. Andreoli","year":"1993","unstructured":"Andreoli, J.-M., Castagnetti, T., Pareschi, R.: Abstract interpretation of linear logic programming. In: Miller, D. (ed.) Proceedings of the International Logic Programming Symposium, Vancouver, Canada, pp. 295\u2013314. MIT Press, Cambridge (1993)"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Andreoli, J.-M., Pareschi, R.: LO and behold! Concurrent structured processes. In: Proceedings of OOPSLA 1990, Ottawa, Canada, October 1990, vol.\u00a025(10), pp. 44\u201356. Published as ACM SIGPLAN Notices (1990)","DOI":"10.1145\/97945.97953"},{"key":"12_CR5","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/BF03037173","volume":"9","author":"J.-M. Andreoli","year":"1991","unstructured":"Andreoli, J.-M., Pareschi, R.: Linear objects: Logical processes with built-in inheritance. New Generation Computing\u00a09, 445\u2013473 (1991)","journal-title":"New Generation Computing"},{"key":"12_CR6","unstructured":"Arcelli, F.: Aspetti di ordine superiore e di metalivello della programmazione logica. PhD thesis, DSI, Universit\u00e1 di Milano (1991)"},{"key":"12_CR7","unstructured":"Arcelli, F., Formato, F.: Implementing higher-order term-rewriting for program transformation in \u03bbProlog. In: Alpuente, Sessa [1], pp. 245\u2013256"},{"key":"12_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-540-73595-3_28","volume-title":"Automated Deduction \u2013 CADE-21","author":"D. Baelde","year":"2007","unstructured":"Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.: The Bedwyr system for model checking over syntactic expressions. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 391\u2013397. Springer, Heidelberg (2007)"},{"issue":"5","key":"12_CR9","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1093\/logcom\/8.5.597","volume":"8","author":"M. Baldoni","year":"1998","unstructured":"Baldoni, M., Giordano, L., Martelli, A.: A modal extension of logic programming: Modularity, beliefs and hypothetical reasoning. J. Log. Comput.\u00a08(5), 597\u2013635 (1998)","journal-title":"J. Log. Comput."},{"key":"12_CR10","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0743-1066(90)90023-X","volume":"8","author":"R. Barbuti","year":"1990","unstructured":"Barbuti, R., Mancarella, P., Pedreschi, D., Turini, F.: A transformational approach to negation in logic programming. Journal of Logic Programming\u00a08, 201\u2013228 (1990)","journal-title":"Journal of Logic Programming"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/978-3-642-14309-0_2","volume-title":"25 Years of Logic Programming in Italy","author":"A. Bossi","year":"2010","unstructured":"Bossi, A., Meo, M.C.: Theoretical Foundations and Semantics. In: Dovier, A., Pontelli, E. (eds.) 25 Years of Logic Programming in Italy. LNCS, pp. 15\u201336. Springer, Heidelberg (2010)"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Delzanno, G., Martelli, M.: On the relations between disjunctive and linear logic programming. Electr. Notes Theor. Comput. Sci.\u00a048 (2001)","DOI":"10.1016\/S1571-0661(04)00150-1"},{"issue":"1","key":"12_CR13","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1017\/S1471068402001254","volume":"2","author":"M. Bozzano","year":"2002","unstructured":"Bozzano, M., Delzanno, G., Martelli, M.: An effective fixpoint semantics for linear logic programs. Theory Pract. Log. Program.\u00a02(1), 85\u2013122 (2002)","journal-title":"Theory Pract. Log. Program."},{"issue":"5-6","key":"12_CR14","first-page":"573","volume":"4","author":"M. Bozzano","year":"2004","unstructured":"Bozzano, M., Delzanno, G., Martelli, M.: Model checking linear logic specifications. TPLP\u00a04(5-6), 573\u2013619 (2004)","journal-title":"TPLP"},{"key":"12_CR15","unstructured":"Bruscoli, P., Guglielmi, A.: Expressiveness of the abstract logic programming language Forum in planning and concurrency. In: Alpuente, M., Barbuti, R., Ramos, I. (eds.) GULP-PRODE (2), pp. 221\u2013237 (1994)"},{"issue":"1","key":"12_CR16","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1093\/logcom\/10.1.75","volume":"10","author":"M. Bugliesi","year":"2000","unstructured":"Bugliesi, M., Delzanno, G., Liquori, L., Martelli, M.: Object calculi in linear logic. J. Log. Comput.\u00a010(1), 75\u2013104 (2000)","journal-title":"J. Log. Comput."},{"key":"12_CR17","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1016\/0743-1066(94)90032-9","volume":"19\/20","author":"M. Bugliesi","year":"1994","unstructured":"Bugliesi, M., Lamma, E., Mello, P.: Modularity in logic programming. J. Log. Program.\u00a019\/20, 443\u2013502 (1994)","journal-title":"J. Log. Program."},{"key":"12_CR18","unstructured":"Cervesato, I.: Petri nets and linear logic: a case study for logic programming. In: Alpuente, Sessa [1], pp. 313\u2013320"},{"key":"12_CR19","first-page":"115","volume-title":"Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming (JICSLP 1998)","author":"I. Cervesato","year":"1998","unstructured":"Cervesato, I.: Proof-theoretic foundation of compilation in logic programming languages. In: Jaffar, J. (ed.) Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming (JICSLP 1998), Manchester, UK, pp. 115\u2013129. MIT Press, Cambridge (1998)"},{"key":"12_CR20","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/3-540-60983-0_5","volume-title":"Extensions of Logic Programming","author":"I. Cervesato","year":"1996","unstructured":"Cervesato, I., Hodas, J.S., Pfenning, F.: Efficient resource management for linear logic proof search. In: Herre, H., Dyckhoff, R., Schroeder-Heister, P. (eds.) ELP 1996. LNCS (LNAI), vol.\u00a01050, pp. 67\u201381. Springer, Heidelberg (1996)"},{"issue":"1-2","key":"12_CR21","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0304-3975(99)00173-5","volume":"232","author":"I. Cervesato","year":"2000","unstructured":"Cervesato, I., Hodas, J.S., Pfenning, F.: Efficient resource management for linear logic proof search. Theoretical Computer Science\u00a0232(1-2), 133\u2013163 (2000); Extended version of [20]","journal-title":"Theoretical Computer Science"},{"key":"12_CR22","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1109\/LICS.1997.614967","volume-title":"Proceedings of the Twelfth Annual Sumposium on Logic in Computer Science (LICS 1997)","author":"I. Cervesato","year":"1997","unstructured":"Cervesato, I., Pfenning, F.: Linear higher-order pre-unification. In: Winskel, G. (ed.) Proceedings of the Twelfth Annual Sumposium on Logic in Computer Science (LICS 1997), Warsaw, Poland, pp. 422\u2013433. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"#cr-split#-12_CR23.1","unstructured":"Cervesato, I., Pfenning, F.: A linear logical framework. Information and Computation (1998);"},{"key":"#cr-split#-12_CR23.2","unstructured":"Special issue with invited papers from LICS 1996, Clarke, E. (ed.)"},{"issue":"5","key":"12_CR24","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1093\/logcom\/13.5.639","volume":"13","author":"I. Cervesato","year":"2003","unstructured":"Cervesato, I., Pfenning, F.: A linear spine calculus. J. Log. Comput.\u00a013(5), 639\u2013688 (2003)","journal-title":"J. Log. Comput."},{"issue":"2-3","key":"12_CR25","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s10817-007-9091-0","volume":"40","author":"K. Chaudhuri","year":"2008","unstructured":"Chaudhuri, K., Pfenning, F., Price, G.: A logical characterization of forward and backward chaining in the inverse method. J. Autom. Reasoning\u00a040(2-3), 133\u2013177 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"12_CR26","unstructured":"Chirimar, J.L.: Proof Theoretic Approach to Specification Languages. PhD thesis, University of Pennsylvania (May 1995)"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Costantini, S., Lanzarone, G.A.: A metalogic programming language. In: ICLP, pp. 218\u2013233 (1989)","DOI":"10.1142\/S0129054190000175"},{"key":"12_CR28","unstructured":"Delzanno, G.: Logic and Object-Oriented Programming in Linear Logic. PhD thesis, Universit\u00e1 di Pisa (February 1997)"},{"key":"12_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1007\/978-3-642-14309-0_7","volume-title":"25 Years of Logic Programming in Italy","author":"G. Delzanno","year":"2010","unstructured":"Delzanno, G., Giacobazzi, R., Ranzato, F.: Static Analysis, Abstract Interpretation and Verification in (Constraint Logic) Programming. In: Dovier, A., Pontelli, E. (eds.) 25 Years of Logic Programming in Italy. LNCS, vol.\u00a06125, pp. 136\u2013158. Springer, Heidelberg (2010)"},{"issue":"1-2","key":"12_CR30","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/S0304-3975(00)00024-4","volume":"258","author":"G. Delzanno","year":"2001","unstructured":"Delzanno, G., Martelli, M.: Proofs as computations in linear logic. Theoretical Computer Science\u00a0258(1-2), 269\u2013297 (2001)","journal-title":"Theoretical Computer Science"},{"key":"12_CR31","series-title":"Lecture Notes in Computer Science","volume-title":"25 Years of Logic Programming in Italy","year":"2010","unstructured":"Dovier, A., Pontelli, E. (eds.): 25 Years of Logic Programming in Italy. LNCS, vol.\u00a06125. Springer, Heidelberg (2010)"},{"issue":"1","key":"12_CR32","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/BF00881900","volume":"11","author":"A.P. Felty","year":"1993","unstructured":"Felty, A.P.: Implementing tactics and tacticals in a higher-order logic programming language. J. Autom. Reasoning\u00a011(1), 41\u201381 (1993)","journal-title":"J. Autom. Reasoning"},{"issue":"4","key":"12_CR33","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0743-1066(85)80003-0","volume":"2","author":"D.M. Gabbay","year":"1985","unstructured":"Gabbay, D.M.: N-Prolog: An extension of Prolog with hypothetical implication II - logical foundations, and negation as failure. J. Log. Program.\u00a02(4), 251\u2013283 (1985)","journal-title":"J. Log. Program."},{"issue":"4","key":"12_CR34","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0743-1066(84)90029-3","volume":"1","author":"D.M. Gabbay","year":"1984","unstructured":"Gabbay, D.M., Reyle, U.: N-Prolog: An extension of Prolog with hypothetical implications I. J. Log. Program.\u00a01(4), 319\u2013355 (1984)","journal-title":"J. Log. Program."},{"key":"12_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/978-3-642-14309-0_11","volume-title":"25 Years of Logic Programming in Italy","author":"M. Gabbrielli","year":"2010","unstructured":"Gabbrielli, M., Palamidessi, C., Valencia, F.D.: Concurrent and Reactive Constraint Programming. In: Dovier, A., Pontelli, E. (eds.) 25 Years of Logic Programming in Italy. LNCS, vol.\u00a06125, pp. 231\u2013253. Springer, Heidelberg (2010)"},{"key":"12_CR36","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":"2","key":"12_CR37","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0743-1066(97)10014-0","volume":"36","author":"L. Giordano","year":"1998","unstructured":"Giordano, L., Olivetti, N.: Combining negation as failure and embedded implications in logic programs. J. Log. Program.\u00a036(2), 91\u2013147 (1998)","journal-title":"J. Log. Program."},{"key":"12_CR38","unstructured":"Guglielmi, A.: Abstract Logic Programming in Linear Logic Independence and Causality in a First Order Calculus. PhD thesis, Universit\u00e1 di Pisa (April 1996)"},{"issue":"1","key":"12_CR39","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. Journal of the Association for Computing Machinery\u00a040(1), 143\u2013184 (1993)","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"4-5","key":"12_CR40","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. J. Funct. Program.\u00a017(4-5), 613\u2013673 (2007)","journal-title":"J. Funct. Program."},{"key":"#cr-split#-12_CR41.1","doi-asserted-by":"crossref","unstructured":"Hodas, J., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Information and Computation??110(2), 327???365 (1994);","DOI":"10.1006\/inco.1994.1036"},{"key":"#cr-split#-12_CR41.2","unstructured":"A preliminary version appeared in the Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pp. 32???42, Amsterdam, The Netherlands (July 1991)"},{"key":"12_CR42","doi-asserted-by":"crossref","unstructured":"Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science\u00a0410(46) (2009)","DOI":"10.1016\/j.tcs.2009.07.041"},{"key":"12_CR43","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1145\/1069774.1069778","volume-title":"PPDP","author":"P. L\u00f3pez","year":"2005","unstructured":"L\u00f3pez, P., Pfenning, F., Polakow, J., Watkins, K.: Monadic concurrent linear logic programming. In: Barahona, P., Felty, A.P. (eds.) PPDP, pp. 35\u201346. ACM, New York (2005)"},{"key":"12_CR44","first-page":"268","volume-title":"Proceedings of the Sixth International Conference on Logic Programming","author":"D. Miller","year":"1989","unstructured":"Miller, D.: Lexical scoping as universal quantification. In: Levi, G., Martelli, M. (eds.) Proceedings of the Sixth International Conference on Logic Programming, Lisbon, Portugal, pp. 268\u2013283. MIT Press, Cambridge (1989)"},{"key":"12_CR45","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/BFb0038698","volume-title":"Extensions of Logic Programming","author":"D. Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. In: Schroeder-Heister, P. (ed.) ELP 1989. LNCS (LNAI), vol.\u00a0475, pp. 253\u2013281. Springer, Heidelberg (1991)"},{"issue":"1-2","key":"12_CR46","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0743-1066(89)90031-9","volume":"6","author":"D. Miller","year":"1989","unstructured":"Miller, D.: A logical analysis of modules in logic programming. Journal of Logic Programming\u00a06(1-2), 79\u2013108 (1989)","journal-title":"Journal of Logic Programming"},{"key":"12_CR47","first-page":"329","volume-title":"Logic and Computer Science","author":"D. Miller","year":"1990","unstructured":"Miller, D.: Abstractions in logic programming. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 329\u2013359. Academic Press, London (1990)"},{"key":"12_CR48","series-title":"LNAI","volume-title":"Extensions of Logic Programming","author":"D. Miller","year":"1994","unstructured":"Miller, D.: A proposal for modules in \u03bbProlog. In: Dyckhoff, R. (ed.) ELP 1993. LNCS (LNAI), vol.\u00a0798. Springer, Heidelberg (1994)"},{"issue":"1","key":"12_CR49","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0304-3975(96)00045-X","volume":"165","author":"D. Miller","year":"1996","unstructured":"Miller, D.: Forum: A multiple-conclusion specification logic. Theoretical Computer Science\u00a0165(1), 201\u2013232 (1996)","journal-title":"Theoretical Computer Science"},{"key":"12_CR50","series-title":"London Mathematical Society Lecture Note","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1017\/CBO9780511550850.004","volume-title":"Linear Logic in Computer Science","author":"D. Miller","year":"2004","unstructured":"Miller, D.: Overview of linear logic programming. In: Ehrhard, T., Girard, J.-Y., Ruet, P., Scott, P. (eds.) Linear Logic in Computer Science. London Mathematical Society Lecture Note, vol.\u00a0316, pp. 119\u2013150. Cambridge University Press, Cambridge (2004)"},{"key":"12_CR51","doi-asserted-by":"publisher","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. Annals of Pure and Applied Logic\u00a051, 125\u2013157 (1991)","journal-title":"Annals of Pure and Applied Logic"},{"key":"12_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/BFb0023886","volume-title":"Logical Foundations of Computer Science - Tver \u201992","author":"A. Momigliano","year":"1992","unstructured":"Momigliano, A.: Minimal negation and Hereditary Harrop Formulae. In: Nerode, A., Taitslin, M.A. (eds.) LFCS 1992. LNCS, vol.\u00a0620, pp. 326\u2013335. Springer, Heidelberg (1992)"},{"key":"12_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-44622-2_28","volume-title":"Computer Science Logic","author":"A. Momigliano","year":"2000","unstructured":"Momigliano, A.: Elimination of negation in a logical framework. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol.\u00a01862, pp. 411\u2013426. Springer, Heidelberg (2000)"},{"key":"12_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/3-540-36576-1_24","volume-title":"Foundations of Software Science and Computational Structures","author":"A. Momigliano","year":"2003","unstructured":"Momigliano, A., Ambler, S.: Multi-level meta-reasoning with higher-order abstract syntax. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 375\u2013391. Springer, Heidelberg (2003)"},{"key":"12_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/978-3-540-24849-1_19","volume-title":"Types for Proofs and Programs","author":"A. Momigliano","year":"2004","unstructured":"Momigliano, A., Tiu, A.F.: Induction and co-induction in sequent calculus. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 293\u2013308. Springer, Heidelberg (2004)"},{"key":"12_CR56","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/S0304-3975(99)00177-2","volume":"232","author":"G. Nadathur","year":"2000","unstructured":"Nadathur, G.: Correspondences between classical, intuitionistic and uniform provability. Theoretical Computer Science\u00a0232, 273\u2013298 (2000)","journal-title":"Theoretical Computer Science"},{"key":"12_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44716-4_1","volume-title":"Functional and Logic Programming","author":"G. Nadathur","year":"2001","unstructured":"Nadathur, G.: The metalanguage \u03bbProlog and its implementation. In: Kuchen, H., Ueda, K. (eds.) FLOPS 2001. LNCS, vol.\u00a02024, pp. 1\u201320. Springer, Heidelberg (2001)"},{"key":"12_CR58","unstructured":"Pareschi, R.: Type-Driven Natural Language Analysis. PhD thesis, University of Edinburgh. University of Pennsylvania, Department of Computer and Information Science, Technical Report No. MS-CIS-89-45 (July 1989)"},{"key":"12_CR59","unstructured":"Pfenning, F.: Computation and deduction. Unpublished lecture notes, p. 217 (Revised March 2001) (May 1992)"},{"key":"12_CR60","volume-title":"Handbook of Automated Reasoning","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F.: Logical frameworks. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning. Elsevier Science Publishers, Amsterdam (1999)"},{"key":"12_CR61","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of the ACM SIGPLAN 1988 Symposium on Language Design and Implementation, Atlanta, Georgia, June 1988, pp. 199\u2013208 (1988)","DOI":"10.1145\/53990.54010"},{"key":"12_CR62","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":"12_CR63","unstructured":"Sch\u00fcrmann, C.: Automating the Meta-Theory of Deductive Systems. PhD thesis, Carnegie-Mellon University, CMU-CS-00-146 (2000)"},{"key":"12_CR64","unstructured":"Warren, O.H.D.: Higher-order extensions to Prolog: Are they needed? In: Hayes, J.E., Michie, D., Pao, Y.-H. (eds.) Machine Intelligence, vol.\u00a010, pp. 441\u2013454. Halsted Press (1982)"},{"key":"12_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/978-3-540-24849-1_23","volume-title":"Types for Proofs and Programs","author":"K. Watkins","year":"2004","unstructured":"Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework: The propositional fragment. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 355\u2013377. Springer, Heidelberg (2004)"},{"key":"12_CR66","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.entcs.2007.11.013","volume":"199","author":"K. Watkins","year":"2008","unstructured":"Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: Specifying properties of concurrent computations in CLF. Electr. Notes Theor. Comput. Sci.\u00a0199, 67\u201387 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","A 25-Year Perspective on Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14309-0_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,30]],"date-time":"2021-10-30T01:17:13Z","timestamp":1635556633000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14309-0_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642143083","9783642143090"],"references-count":68,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14309-0_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}