{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:50:57Z","timestamp":1725490257456},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540749141"},{"type":"electronic","value":"9783540749158"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74915-8_31","type":"book-chapter","created":{"date-parts":[[2007,8,24]],"date-time":"2007-08-24T05:13:35Z","timestamp":1187932415000},"page":"405-419","source":"Crossref","is-referenced-by-count":24,"title":["From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic"],"prefix":"10.1007","author":[{"given":"Dale","family":"Miller","sequence":"first","affiliation":[]},{"given":"Alexis","family":"Saurin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"31_CR1","first-page":"431","volume-title":"LICS 1999","author":"S. Abramsky","year":"1999","unstructured":"Abramsky, S., Melli\u00e8s, P.-A.: Concurrent games and full completeness. In: LICS 1999, pp. 431\u2013442. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"31_CR2","unstructured":"Andreoli, J.-M., Pareschi, R.: Linear objects: Logical processes with built-in inheritance. In: Proceeding of ICLP 1990, Jerusalem (1990)"},{"key":"31_CR3","unstructured":"Andreoli, J.-M.: Proposal for a Synthesis of Logic and Object-Oriented Programming Paradigms. PhD thesis, University of Paris VI (1990)"},{"issue":"3","key":"31_CR4","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. of Logic and Computation\u00a02(3), 297\u2013347 (1992)","journal-title":"J. of Logic and Computation"},{"key":"31_CR5","unstructured":"Baelde, D., Miller, D.: Least and greatest fixed points in LL (submitted, April 2007)"},{"key":"31_CR6","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/351240.351262","volume-title":"ICFP 2000","author":"P.-L. Curien","year":"2000","unstructured":"Curien, P.-L., Herbelin, H.: The duality of computation. In: ICFP 2000. Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, New York, NY, USA, pp. 233\u2013243. ACM Press, New York (2000)"},{"key":"31_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/BFb0022564","volume-title":"Computational Logic and Proof Theory","author":"V. Danos","year":"1993","unstructured":"Danos, V., Joinet, J.-B., Schellinx, H.: The structure of exponentials: Uncovering the dynamics of linear logic proofs. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol.\u00a0713, pp. 159\u2013171. Springer, Heidelberg (1993)"},{"key":"31_CR8","series-title":"London Mathematical Society Lecture Notes 222","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1017\/CBO9780511629150.011","volume-title":"Workshop on Linear Logic","author":"V. Danos","year":"1995","unstructured":"Danos, V., Joinet, J.-B., Schellinx, H.: LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implication. In: Girard,, Lafont,, Regnier (eds.) Workshop on Linear Logic. London Mathematical Society Lecture Notes 222, pp. 211\u2013224. Cambridge University Press, Cambridge (1995)"},{"issue":"3","key":"31_CR9","doi-asserted-by":"publisher","first-page":"755","DOI":"10.2307\/2275572","volume":"62","author":"V. Danos","year":"1997","unstructured":"Danos, V., Joinet, J.-B., Schellinx, H.: A new deconstructive logic: Linear logic. Journal of Symbolic Logic\u00a062(3), 755\u2013807 (1997)","journal-title":"Journal of Symbolic Logic"},{"key":"31_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/11780342_19","volume-title":"Logical Approaches to Computational Barriers","author":"R. Dyckhoff","year":"2006","unstructured":"Dyckhoff, R., Lengrand, S.: LJQ: a strongly focused calculus for intuitionistic logic. In: Beckmann, A., Berger, U., L\u00f6we, B., Tucker, J.V. (eds.) CiE 2006. LNCS, vol.\u00a03988, pp. 173\u2013185. Springer, Heidelberg (2006)"},{"key":"31_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y.: Linear logic. Theoretical Computer Science\u00a050, 1\u2013102 (1987)","journal-title":"Theoretical Computer Science"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Girard, J.-Y.: Light linear logic. Information and Computation\u00a0143 (1998)","DOI":"10.1006\/inco.1998.2700"},{"issue":"3","key":"31_CR13","first-page":"301","volume":"11","author":"J.-Y. Girard","year":"2001","unstructured":"Girard, J.-Y.: Locus solum. MSCS\u00a011(3), 301\u2013506 (2001)","journal-title":"MSCS"},{"key":"31_CR14","unstructured":"Herbelin, H.: S\u00e9quents qu\u2019on calcule: de l\u2019interpr\u00e9tation du calcul des s\u00e9quents comme calcul de lambda-termes et comme calcul de strat\u00e9gies gagnantes. PhD thesis, Universit\u00e9 Paris 7 (1995)"},{"key":"31_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11590156_42","volume-title":"FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science","author":"R. Jagadeesan","year":"2005","unstructured":"Jagadeesan, R., Nadathur, G., Saraswat, V.: Testing concurrent systems: An interpretation of intuitionistic logic. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol.\u00a03821, Springer, Heidelberg (2005)"},{"issue":"1-2","key":"31_CR16","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.tcs.2003.10.018","volume":"318","author":"Y. Lafont","year":"2004","unstructured":"Lafont, Y.: Soft linear logic and polynomial time. TCS\u00a0318(1-2), 163\u2013180 (2004)","journal-title":"TCS"},{"key":"31_CR17","unstructured":"Laurent, O.: Etude de la polarisation en logique. Th\u00e8se de doctorat, Universit\u00e9 Aix-Marseille\u00a0II (March 2002)"},{"key":"31_CR18","unstructured":"Laurent, O.: A proof of the focalization property of LL. Unpublished Note (May 2004)"},{"key":"31_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/978-3-540-74915-8_34","volume-title":"CSL 2007","author":"C. Liang","year":"2007","unstructured":"Liang, C., Miller, D.: Focusing and polarization in intuitionistic logic. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 451\u2013465. Springer, Heidelberg (2007)"},{"issue":"1","key":"31_CR20","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"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74915-8_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:45:52Z","timestamp":1619520352000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74915-8_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540749141","9783540749158"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74915-8_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}