{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T23:04:43Z","timestamp":1746745483182},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642396335"},{"type":"electronic","value":"9783642396342"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_28","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T13:52:36Z","timestamp":1374501156000},"page":"386-401","source":"Crossref","is-referenced-by-count":5,"title":["Subformula Linking as an Interaction Method"],"prefix":"10.1007","author":[{"given":"Kaustuv","family":"Chaudhuri","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"28_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"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Baelde, D.: Least and greatest fixed points in linear logic. ACM Trans. on Computational Logic\u00a013(1) (April 2012)","DOI":"10.1145\/2071368.2071370"},{"issue":"3","key":"28_CR3","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/s001650050049","volume":"11","author":"Y. Bertot","year":"1999","unstructured":"Bertot, Y.: The CtCoq system: Design and architecture. Formal Aspects of Computing\u00a011(3), 225\u2013243 (1999)","journal-title":"Formal Aspects of Computing"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/3-540-57887-0_94","volume-title":"Theoretical Aspects of Computer Software","author":"Y. Bertot","year":"1994","unstructured":"Bertot, Y., Kahn, G., Th\u00e9ry, L.: Proof by pointing. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol.\u00a0789, pp. 141\u2013160. Springer, Heidelberg (1994)"},{"key":"28_CR5","unstructured":"Boespflug, M., Carbonneaux, Q., Hermant, O.: The \u03bb\u03a0-calculus modulo as a universal proof language. In: Pichardie, D., Weber, T. (eds.) Proceedings of PxTP 2012: Proof Exchange for Theorem Proving, pp. 28\u201343 (2012)"},{"key":"28_CR6","unstructured":"Chaudhuri, K.: Profound (2013), \n                    \n                      http:\/\/chaudhuri.info\/software\/profound\/"},{"key":"28_CR7","unstructured":"Chaudhuri, K., Guenot, N., Stra\u00dfburger, L.: The Focused Calculus of Structures. In: Computer Science Logic: 20th Annual Conference of the EACSL, Leibniz International Proceedings in Informatics (LIPIcs), pp. 159\u2013173. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (September 2011)"},{"issue":"2-3","key":"28_CR8","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. of Automated Reasoning\u00a040(2-3), 133\u2013177 (2008)","journal-title":"J. of Automated Reasoning"},{"key":"28_CR9","unstructured":"Gacek, A.: The Abella system and homepage (2009), \n                    \n                      http:\/\/abella.cs.umn.edu\/"},{"key":"28_CR10","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":"28_CR11","doi-asserted-by":"crossref","unstructured":"Thery, G.K.L., Bertot, Y.: Real theorem provers deserve real user-interfaces. In: Proceedings of the Fifth ACM SIGSOFT Symposium on Software Development Environments. Software Engineering Notes, vol.\u00a017(5). ACM Press (1992)","DOI":"10.1145\/142868.143760"},{"issue":"46","key":"28_CR12","doi-asserted-by":"publisher","first-page":"4747","DOI":"10.1016\/j.tcs.2009.07.041","volume":"410","author":"C. Liang","year":"2009","unstructured":"Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science\u00a0410(46), 4747\u20134768 (2009)","journal-title":"Theoretical Computer Science"},{"key":"28_CR13","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-89439-1_12","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S. McLaughlin","year":"2008","unstructured":"McLaughlin, S., Pfenning, F.: Imogen: Focusing the polarized focused inverse method for intuitionistic propositional logic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 174\u2013181. Springer, Heidelberg (2008)"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"Snow, Z., Baelde, D., Nadathur, G.: A meta-programming approach to realizing dependently typed logic programming. In: ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), pp. 187\u2013198 (2010)","DOI":"10.1145\/1836089.1836113"},{"key":"28_CR15","unstructured":"Stra\u00dfburger, L.: Linear Logic and Noncommutativity in the Calculus of Structures. PhD thesis, Technische Universit\u00e4t Dresden (2003)"},{"key":"28_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-642-02273-9_23","volume-title":"Typed Lambda Calculi and Applications","author":"L. Stra\u00dfburger","year":"2009","unstructured":"Stra\u00dfburger, L.: Some observations on the proof theory of second order propositional multiplicative linear logic. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol.\u00a05608, pp. 309\u2013324. Springer, Heidelberg (2009)"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Stump, A.: Proof checking technology for satisfiability modulo theories. In: Abel, A., Urban, C. (eds.) Logical Frameworks and Meta-Languages: Theory and Practice (2008)","DOI":"10.1016\/j.entcs.2008.12.121"},{"key":"28_CR18","unstructured":"Tiu, A.: A Logical Framework for Reasoning about Logical Specifications. PhD thesis, Pennsylvania State University (May 2004)"},{"key":"28_CR19","unstructured":"Troelstra, A.S.: Lectures on Linear Logic. CSLI Lecture Notes 29, Center for the Study of Language and Information, Stanford, California (1992)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39634-2_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:50:48Z","timestamp":1558317048000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}