{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:46:41Z","timestamp":1725454001138},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540638889"},{"type":"electronic","value":"9783540696612"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0000492","type":"book-chapter","created":{"date-parts":[[2005,10,5]],"date-time":"2005-10-05T06:30:36Z","timestamp":1128493836000},"page":"494-508","source":"Crossref","is-referenced-by-count":2,"title":["Algebraic composition and refinement of proofs"],"prefix":"10.1007","author":[{"given":"Martin","family":"Simons","sequence":"first","affiliation":[]},{"given":"Michel","family":"Sintzoff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,9,7]]},"reference":[{"key":"34_CR1","unstructured":"Abramsky, S. (1994), Interaction categories and communicating sequential processes, in A. W. Roscoe, ed., \u2018A Classical Mind: Essays in Honour of C.A.R. Hoare', Prentice Hall, pp. 1\u201316."},{"key":"34_CR2","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1017\/S0960129500000189","volume":"3","author":"S. Abramsky","year":"1993","unstructured":"Abramsky, S. & Vickers, S. (1993), \u2018Quantales, observational logic and process semantics', Mathematical Structures in Computer Science 3, 161\u2013227.","journal-title":"Mathematical Structures in Computer Science"},{"key":"34_CR3","doi-asserted-by":"crossref","unstructured":"Bird, R. & de Moor, O. (1997), Algebra of Programming, Prentice Hall.","DOI":"10.1007\/978-3-642-61455-2_12"},{"issue":"2","key":"34_CR4","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0022-4049(95)00160-3","volume":"114","author":"J. R. B. Cockett","year":"1997","unstructured":"Cockett, J. R. B. & Seely, R. A. G. (1997), \u2018Weakly distributive categories', Journal of Pure and Applied Algebra 114(2), 133\u2013173.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"34_CR5","unstructured":"Davey, B. A. & Priestley, H. A. (1990), Introduction to Lattices and Order, Cambridge University Press."},{"key":"34_CR6","unstructured":"Do\u0161en, K. & Schroeder-Heister, P., eds (1993), Substructural Logics, Oxford Science Publications."},{"key":"34_CR7","doi-asserted-by":"crossref","unstructured":"Dunn, J. M. (1990), Gaggle theory: An abstraction of Galois connections and residuation, with applications to negation, implication, and various logical operators, in J. van Eijck, ed., \u2018European Workshop on Logics in AI (JELIA'90)', LNCS 478, Springer Verlag.","DOI":"10.1007\/BFb0018431"},{"key":"34_CR8","unstructured":"Dunn, J. M. (1993), Partial gaggles applied to logics with restricted structural rules, in Do\u0161en & Schroeder-Heister (1993), pp. 63\u2013108."},{"key":"34_CR9","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/BF01888221","volume":"2","author":"W. J. Hesselink","year":"1990","unstructured":"Hesselink, W. J. (1990), \u2018Axioms and models of linear logic', Formal Aspects of Computing 2, 139\u2013166.","journal-title":"Formal Aspects of Computing"},{"key":"34_CR10","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/0020-0190(87)90106-2","volume":"24","author":"C. A. R. Hoare","year":"1987","unstructured":"Hoare, C. A. R. & He, J. (1987), \u201cThe weakest prespecification', Information Processing Letters 24, 127\u2013132.","journal-title":"Information Processing Letters"},{"key":"34_CR11","unstructured":"Jones, C. B. (1990), Systematic Software Development Using VDM, second edn, Prentice Hall."},{"key":"34_CR12","unstructured":"Kleene, S. C. (1971), Introduction to Metamathematics, sixth reprint edn, North Holland."},{"issue":"7","key":"34_CR13","doi-asserted-by":"crossref","first-page":"600","DOI":"10.1080\/00029890.1995.12004627","volume":"102","author":"L. Lamport","year":"1994","unstructured":"Lamport, L. (1994), \u2018How to write a proof', American Mathematical Monthly 102(7), 600\u2013608.","journal-title":"American Mathematical Monthly"},{"issue":"4","key":"34_CR14","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/BF01213535","volume":"8","author":"A. P. Martin","year":"1997","unstructured":"Martin, A. P., Gardiner, P. & Woodcock, J. C. P. (1997), \u2018A tactic calculus \u2014 abridged version', Formal Aspects of Computing 8(4), 479\u2013489.","journal-title":"Formal Aspects of Computing"},{"key":"34_CR15","unstructured":"Ono, H. (1993), Semantics of substructural logics, in Do\u0161en & Schroeder-Heister (1993), pp. 259\u2013291."},{"key":"34_CR16","doi-asserted-by":"crossref","unstructured":"Pratt, V. (1995), Chu spaces and their interpretation as concurrent objects, in J. van Leeuwen, ed., \u2018Computer Science Today: Recent Trends and Developments', LNCS 1000, Springer Verlag, pp. 392\u2013405.","DOI":"10.1007\/BFb0015256"},{"key":"34_CR17","unstructured":"Rosenthal, K. I. (1990), Quantales and their Application, Longman Scientific & Technical."},{"key":"34_CR18","unstructured":"Simons, M. (1997a), The Presentation of Formal Proofs, GMD-Bericht Nr. 278, Oldenbourg Verlag."},{"key":"34_CR19","doi-asserted-by":"crossref","unstructured":"Simons, M. (1997b), Proof presentation for Isabelle, in E. L. Gunter & A. Felty, eds, \u201cTheorem Proving in Higher Order Logics \u2014 10th International Conference', LNCS 1275, Springer Verlag, pp. 259\u2013274.","DOI":"10.1007\/BFb0028399"},{"issue":"1","key":"34_CR20","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/BF01211052","volume":"8","author":"M. Simons","year":"1996","unstructured":"Simons, M. & Weber, M. (1996), \u2018An approach to literate and structured formal developments', Formal Aspects of Computing 8(1), 86\u2013107.","journal-title":"Formal Aspects of Computing"},{"key":"34_CR21","doi-asserted-by":"crossref","unstructured":"Sintzoff, M. (1993), Endomorphic typing, in B. M\u00f6ller, H. A. Partsch & S. A. Schumann, eds, 'Formal Program Development', LNCS 755, Springer Verlag, pp. 305\u2013323.","DOI":"10.1007\/3-540-57499-9_24"},{"key":"34_CR22","unstructured":"Troelstra, A. S. (1992), Lectures on Linear Logic, number 29 in \u2018CSLI Lecture Notes', CSLI."},{"key":"34_CR23","unstructured":"Vickers, S. (1989), Topology via Logic, Cambridge University Press."},{"key":"34_CR24","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/BF01212485","volume":"5","author":"M. Weber","year":"1993","unstructured":"Weber, M. (1993), \u2018Definition and basic properties of the Deva meta-calculus', Formal Aspects of Computing 5, 391\u2013431.","journal-title":"Formal Aspects of Computing"},{"key":"34_CR25","doi-asserted-by":"crossref","unstructured":"Weber, M., Simons, M. & Lafontaine, C. (1993), The Generic Development Language Deva: Presentation and Case Studies, LNCS 738, Springer Verlag.","DOI":"10.1007\/3-540-57335-6"},{"key":"34_CR26","doi-asserted-by":"crossref","first-page":"41","DOI":"10.2307\/2274953","volume":"55","author":"D. Yetter","year":"1990","unstructured":"Yetter, D. (1990), \u2018Quantales and (non-commutative) linear logic', The Journal of Symbolic Logic 55, 41\u201364.","journal-title":"The Journal of Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0000492","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,9]],"date-time":"2020-04-09T22:22:17Z","timestamp":1586470937000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0000492"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540638889","9783540696612"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/bfb0000492","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}