{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:56:08Z","timestamp":1725562568943},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540221647"},{"type":"electronic","value":"9783540248491"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24849-1_23","type":"book-chapter","created":{"date-parts":[[2010,8,8]],"date-time":"2010-08-08T20:34:24Z","timestamp":1281299664000},"page":"355-377","source":"Crossref","is-referenced-by-count":41,"title":["A Concurrent Logical Framework: The Propositional Fragment"],"prefix":"10.1007","author":[{"given":"Kevin","family":"Watkins","sequence":"first","affiliation":[]},{"given":"Iliano","family":"Cervesato","sequence":"additional","affiliation":[]},{"given":"Frank","family":"Pfenning","sequence":"additional","affiliation":[]},{"given":"David","family":"Walker","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24849-1_1","volume-title":"Types for Proofs and Programs","author":"R. Adams","year":"2004","unstructured":"Adams, R.: A modular hierarchy of logical frameworks. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 1\u201316. Springer, Heidelberg (2004)"},{"issue":"3","key":"23_CR2","doi-asserted-by":"publisher","first-page":"197","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. Journal of Logic and Computation\u00a02(3), 197\u2013347 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"23_CR3","unstructured":"Asperti, A.: A logic for concurrency. Technical report, Department of Computer Science, University of Pisa (1987)"},{"key":"23_CR4","first-page":"59","volume-title":"Proceedings of the seventeenth Symposium on Principles of Programming Languages","author":"A. Asperti","year":"1990","unstructured":"Asperti, A., Ferrari, G., Gorrieri, R.: Implicative formulae in the \u2018proofs as computations\u2019 analogy. In: Proceedings of the seventeenth Symposium on Principles of Programming Languages, San Francisco, January 1990, pp. 59\u201371. ACM Press, New York (1990)"},{"key":"23_CR5","unstructured":"Barber, A.: Dual intuitionistic linear logic. Technical Report ECS-LFCS-96-347, Department of Computer Science, University of Edinburgh (September 1996)"},{"key":"23_CR6","volume-title":"Handbook of Philosophical Logic","author":"D. Basin","year":"2001","unstructured":"Basin, D., Matthews, S.: Logical frameworks. In: Handbook of Philosophical Logic, 2nd edn., Kluwer Academic Publishers, Dordrecht (2001)","edition":"2"},{"key":"23_CR7","first-page":"51","volume-title":"Proceedings of the International Logic Programming Symposium (ILPS 1995)","author":"Y. Bekkers","year":"1995","unstructured":"Bekkers, Y., Tarau, P.: Monadic constructs for logic programming. In: Lloyd, J. (ed.) Proceedings of the International Logic Programming Symposium (ILPS 1995), Portland, Oregon, December 1995, pp. 51\u201365. MIT Press, Cambridge (1995)"},{"key":"23_CR8","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/0304-3975(94)00104-9","volume":"135","author":"G. Bellin","year":"1994","unstructured":"Bellin, G., Scott, P.J.: On the \u03c0-calculus and linear logic. Theoretical Computer Science\u00a0135, 11\u201365 (1994)","journal-title":"Theoretical Computer Science"},{"key":"23_CR9","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1109\/LICS.1996.561458","volume-title":"Proceedings of the 11th Annual Symposium on Logic in Computer Science","author":"P.N. Benton","year":"1996","unstructured":"Benton, P.N., Wadler, P.: Linear logic, monads, and the lambda calculus. In: Clarke, E. (ed.) Proceedings of the 11th Annual Symposium on Logic in Computer Science, New Brunswick, New Jersey, July 1996, pp. 420\u2013431. IEEE Computer Society Press, Los Alamitos (1996)"},{"issue":"1\u20132","key":"23_CR10","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1006\/inco.1999.2819","volume":"156","author":"R. Bruni","year":"2000","unstructured":"Bruni, R., Montanari, U.: Zero-safe nets: Comparing the collective and individual token approaches. Information and Computation\u00a0156(1\u20132), 46\u201389 (2000)","journal-title":"Information and Computation"},{"key":"23_CR11","unstructured":"Cervesato, I.: Petri nets and linear logic: a case study for logic programming. In: Alpuente, M., Sessa, M.I. (eds.) Proceedings of the 1995 Joint Conference on Declarative Programming \u2014 GULP-PRODE 1995, Marina di Vietri, Italy, pp. 313\u2013318 (1995)"},{"key":"23_CR12","unstructured":"Cervesato, I.: A Linear Logical Framework. PhD thesis, Dipartimento di Informatica, Universit\u00e0 di Torino (February 1996)"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/3-540-45116-1_18","volume-title":"Information Assurance in Computer Networks. Methods, Models and Architectures for Network Security","author":"I. Cervesato","year":"2001","unstructured":"Cervesato, I.: Typed MSR: Syntax and examples. In: Gorodetski, V.I., Skormin, V.A., Popyack, L.J. (eds.) MMM-ACNS 2001. LNCS, vol.\u00a02052, pp. 159\u2013177. Springer, Heidelberg (2001)"},{"issue":"1","key":"23_CR14","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1006\/inco.2001.2951","volume":"179","author":"I. Cervesato","year":"2002","unstructured":"Cervesato, I., Pfenning, F.: A linear logical framework. Information & Computation\u00a0179(1), 19\u201375 (2002)","journal-title":"Information & Computation"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Pfenning, F., Walker, D., Watkins, K.: A concurrent logical framework II: Examples and applications. Technical Report CMU-CS-02- 102, Department of Computer Science, Carnegie Mellon University (2002)","DOI":"10.21236\/ADA418538"},{"key":"23_CR16","unstructured":"Chirimar, J.L.: Proof Theoretic Approach to Specification Languages. PhD thesis, University of Pennsylvania (May 1995)"},{"key":"23_CR17","first-page":"131","volume-title":"Logical Environment","author":"N.G. Bruijn de","year":"1993","unstructured":"de Bruijn, N.G.: Algorithmic definition of lambda-typed lambda calculus. In: Huet, G., Plotkin, G. (eds.) Logical Environment, pp. 131\u2013145. Cambridge University Press, Cambridge (1993)"},{"key":"23_CR18","first-page":"214","volume-title":"Logical Frameworks","author":"A. Felty","year":"1991","unstructured":"Felty, A.: Encoding dependent types in an intuitionistic logic. In: Huet, G., Plotkin, G.D. (eds.) Logical Frameworks, pp. 214\u2013251. Cambridge University Press, Cambridge (1991)"},{"issue":"4","key":"23_CR19","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1145\/4472.4478","volume":"7","author":"R.H. Halstead","year":"1985","unstructured":"Halstead, R.H.: Multilisp: A language for parallel symbolic computation. ACM Transactions on Programming Languages and Systems\u00a07(4), 501\u2013539 (1985)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"23_CR20","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"},{"key":"#cr-split#-23_CR21.1","doi-asserted-by":"crossref","unstructured":"Hodas, J., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Information and Computation\u00a0110(2), 327\u2013365 (1994);","DOI":"10.1006\/inco.1994.1036"},{"key":"#cr-split#-23_CR21.2","unstructured":"A preliminary version appeared in the Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, Amsterdam, The Netherlands, pp. 32\u201342 (July 1991)"},{"issue":"2","key":"23_CR22","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/S0304-3975(00)00095-5","volume":"253","author":"F. Honsell","year":"2001","unstructured":"Honsell, F., Miculan, M., Scagnetto, I.: Pi-calculus in (co)inductive type theories. Theoretical Computer Science\u00a0253(2), 239\u2013285 (2001)","journal-title":"Theoretical Computer Science"},{"issue":"6","key":"23_CR23","doi-asserted-by":"publisher","first-page":"809","DOI":"10.1093\/logcom\/8.6.809","volume":"8","author":"S. Ishtiaq","year":"1998","unstructured":"Ishtiaq, S., Pym, D.: A relevant analysis of natural deduction. Journal of Logic and Computation\u00a08(6), 809\u2013838 (1998)","journal-title":"Journal of Logic and Computation"},{"key":"23_CR24","first-page":"279","volume-title":"Proceedings of the 1993 International Logic Programming Symposium","author":"N. Kobayashi","year":"1993","unstructured":"Kobayashi, N., Yonezawa, A.: ACL \u2014 A concurrent linear logic programming paradigm. In: Miller, D. (ed.) Proceedings of the 1993 International Logic Programming Symposium, Vancouver, Canada, pp. 279\u2013294. MIT Press, Cambridge (1993)"},{"issue":"2","key":"23_CR25","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1017\/S0956796802004525","volume":"13","author":"Z. Luo","year":"2003","unstructured":"Luo, Z.: PAL+: A lambda-free logical framework. Journal of Functional Programming\u00a013(2), 317\u2013338 (2003)","journal-title":"Journal of Functional Programming"},{"key":"23_CR26","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1017\/S0960129500000062","volume":"1","author":"N. Mart\u00ed-Oliet","year":"1991","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: From Petri nets to linear logic. Mathematical Structures in Computer Science\u00a01, 66\u2013101 (1991); Revised version of paper in LNCS 389","journal-title":"Mathematical Structures in Computer Science"},{"issue":"4","key":"23_CR27","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1142\/S0129054191000182","volume":"2","author":"N. Mart\u00ed-Oliet","year":"1991","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: From Petri nets to linear logic through categories: A survey. Journal on Foundations of Computer Science\u00a02(4), 297\u2013399 (1991)","journal-title":"Journal on Foundations of Computer Science"},{"key":"23_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/3-540-56454-3_13","volume-title":"Extensions of Logic Programming","author":"D. Miller","year":"1993","unstructured":"Miller, D.: The \u03c0-calculus as a theory in linear logic: Preliminary results. In: Lamma, E., Mello, P. (eds.) ELP 1992. LNCS, vol.\u00a0660, pp. 242\u2013265. Springer, Heidelberg (1993)"},{"key":"23_CR29","volume-title":"Communicating and Mobile Systems: the \u03c0-Calculus","author":"R. Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems: the \u03c0-Calculus. Cambridge University Press, Cambridge (1999)"},{"key":"23_CR30","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/LICS.1989.39155","volume-title":"Proceedings of the Fourth Symposium on Logic in Computer Science","author":"E. Moggi","year":"1989","unstructured":"Moggi, E.: Computational lambda calculus and monads. In: Proceedings of the Fourth Symposium on Logic in Computer Science. Asilomar, California, June 1989, pp. 14\u201323. IEEE Computer Society Press, Los Alamitos (1989)"},{"issue":"1","key":"23_CR31","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Information and Computation\u00a093(1), 55\u201392 (1991)","journal-title":"Information and Computation"},{"key":"23_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/3-540-61064-2_33","volume-title":"Trees in Algebra and Programming - CAAP \u201996","author":"F. Pfenning","year":"1996","unstructured":"Pfenning, F.: The practice of logical frameworks. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol.\u00a01059, pp. 119\u2013134. Springer, Heidelberg (1996)"},{"issue":"1\/2","key":"23_CR33","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1006\/inco.1999.2832","volume":"157","author":"F. Pfenning","year":"2000","unstructured":"Pfenning, F.: Structural cut elimination I. intuitionistic and classical logic. Information and Computation\u00a0157(1\/2), 84\u2013141 (2000)","journal-title":"Information and Computation"},{"key":"23_CR34","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1109\/LICS.2001.932499","volume-title":"Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS 2001)","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F.: Intensionality, extensionality, and proof irrelevance in modal type theory. In: Halpern, J. (ed.) Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS 2001), Boston, MA, June 2001, pp. 221\u2013230. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"23_CR35","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: Logical frameworks. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1063\u20131147. Elsevier Science and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50019-9"},{"key":"23_CR36","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1017\/S0960129501003322","volume":"11","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science\u00a011, 511\u2013540 (2001); Notes to an invited talk at the Workshop on Intuitionistic Modal Logics and Applications (IMLA 1999), Trento, Italy (July 1999)","journal-title":"Mathematical Structures in Computer Science"},{"key":"23_CR37","unstructured":"Reed, J.: Proof irrelevance and strict definitions in a logical framework. Technical Report CMU-CS-02-153, Computer Science Department, Carnegie Mellon University (2002)"},{"key":"23_CR38","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511574962","volume-title":"Concurrent Programming in ML","author":"J.H. Reppy","year":"1999","unstructured":"Reppy, J.H.: Concurrent Programming in ML. Cambridge University Press, Cambridge (1999)"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24849-1_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:57:41Z","timestamp":1605761861000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24849-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540221647","9783540248491"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24849-1_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}