{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T23:11:10Z","timestamp":1784848270795,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540755586","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75560-9_9","type":"book-chapter","created":{"date-parts":[[2007,10,6]],"date-time":"2007-10-06T05:36:46Z","timestamp":1191649006000},"page":"92-106","source":"Crossref","is-referenced-by-count":23,"title":["Least and Greatest Fixed Points in Linear Logic"],"prefix":"10.1007","author":[{"given":"David","family":"Baelde","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dale","family":"Miller","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"3","key":"9_CR1","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"},{"issue":"3-4","key":"9_CR2","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(3-4), 445\u2013473 (1991)","journal-title":"New Generation Computing"},{"issue":"3","key":"9_CR3","doi-asserted-by":"publisher","first-page":"841","DOI":"10.1145\/322326.322339","volume":"29","author":"K.R. Apt","year":"1982","unstructured":"Apt, K.R., van Emden, M.H.: Contributions to the theory of logic programming. J. of the ACM\u00a029(3), 841\u2013862 (1982)","journal-title":"J. of the ACM"},{"key":"9_CR4","series-title":"LNAI","first-page":"391","volume-title":"21th Conference on Automated Deduction","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.) 21th Conference on Automated Deduction. LNCS (LNAI), vol.\u00a04603, pp. 391\u2013397. Springer, Heidelberg (2007)"},{"key":"9_CR5","unstructured":"Baelde, D., Miller, D.: Least and greatest fixed points in linear logic: extended version. Technical report, available from the first author\u2019s web page (April 2007)"},{"key":"9_CR6","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":"9_CR7","first-page":"68","volume-title":"The Collected Papers of Gerhard Gentzen","author":"G. Gentzen","year":"1969","unstructured":"Gentzen, G.: Investigations into logical deductions. In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen, pp. 68\u2013131. North-Holland, Amsterdam (1969)"},{"key":"9_CR8","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":"9_CR9","unstructured":"Girard, J.-Y.: A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs.stanford.edu. (February 1992)"},{"key":"9_CR10","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0168-0072(93)90093-S","volume":"59","author":"J.-Y. Girard","year":"1993","unstructured":"Girard, J.-Y.: On the unity of logic. Annals of Pure and Applied Logic\u00a059, 201\u2013217 (1993)","journal-title":"Annals of Pure and Applied Logic"},{"key":"9_CR11","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":"9_CR12","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1017\/S096012950100336X","volume":"11","author":"J.-Y. Girard","year":"2001","unstructured":"Girard, J.-Y.: Locus solum. Mathematical Structures in Computer Science\u00a011(3), 301\u2013506 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"issue":"2","key":"9_CR13","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1006\/inco.1994.1036","volume":"110","author":"J. Hodas","year":"1994","unstructured":"Hodas, J., Miller, D.: Logic programming in a fragment of intuitionistic linear logic. Information and Computation\u00a0110(2), 327\u2013365 (1994)","journal-title":"Information and Computation"},{"issue":"1-2","key":"9_CR14","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. Theoretical Computer Science\u00a0318(1-2), 163\u2013180 (2004)","journal-title":"Theoretical Computer Science"},{"key":"9_CR15","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":"9_CR16","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":"9_CR17","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0304-3975(99)00171-1","volume":"232","author":"R. McDowell","year":"2000","unstructured":"McDowell, R., Miller, D.: Cut-elimination for a logic with definitions and induction. Theoretical Computer Science\u00a0232, 91\u2013119 (2000)","journal-title":"Theoretical Computer Science"},{"key":"9_CR18","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":"9_CR19","doi-asserted-by":"crossref","unstructured":"Miller, D., Saurin, A.: A game semantics for proof search: Preliminary results. In: Proceedings of the Mathematical Foundations of Programming Semantics (MFPS) (2005)","DOI":"10.1016\/j.entcs.2005.11.072"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/978-3-540-74915-8_31","volume-title":"CSL 2007","author":"D. Miller","year":"2007","unstructured":"Miller, D., Saurin, A.: From proofs to focused proofs: a modular proof of focalization in linear logic. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 405\u2013419. Springer, Heidelberg (2007)"},{"key":"9_CR21","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.: 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":"9_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11591191_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"E. Pimentel","year":"2005","unstructured":"Pimentel, E., Miller, D.: On the specification of sequent systems. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 352\u2013366. Springer, Heidelberg (2005)"},{"key":"9_CR23","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1109\/LICS.1993.287585","volume-title":"Eighth Annual Symposium on Logic in Computer Science","author":"P. Schroeder-Heister","year":"1993","unstructured":"Schroeder-Heister, P.: Rules of definitional reflection. In: Vardi, M. (ed.) Eighth Annual Symposium on Logic in Computer Science, pp. 222\u2013232. IEEE Computer Society Press, Los Alamitos (1993)"},{"key":"9_CR24","unstructured":"Stirling, C.: Games for bisimulation and model checking. Notes for Mathfit Workshop on Finite Model Theory, University of Wales, Swansea (July 1996)"},{"key":"9_CR25","unstructured":"Tiu, A.: A Logical Framework for Reasoning about Logical Specifications. PhD thesis, Pennsylvania State University (May 2004)"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/11539452_7","volume-title":"CONCUR 2005","author":"A. Tiu","year":"2005","unstructured":"Tiu, A.: Model checking for \u03c0-calculus using proof search. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 36\u201350. Springer, Heidelberg (2005)"},{"key":"9_CR27","unstructured":"Tiu, A., Nadathur, G., Miller, D.: Mixing finite success and finite failure in an automated prover. In: ESHOL 2005, pp. 79\u201398 (December 2005)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75560-9_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:24:50Z","timestamp":1619519090000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75560-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540755586"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75560-9_9","relation":{},"subject":[]}}