{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:12:39Z","timestamp":1725631959368},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615873"},{"type":"electronic","value":"9783540706410"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105394","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T16:17:00Z","timestamp":1320855420000},"page":"17-32","source":"Crossref","is-referenced-by-count":2,"title":["A comparison of HOL and ALF formalizations of a categorical coherence theorem"],"prefix":"10.1007","author":[{"given":"Sten","family":"Agerholm","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ilya","family":"Beylin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Dybjer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"unstructured":"Sten Agerholm. Formalizing a proof of coherence for monoidal categories. Draft manuscript, available from \/\/ftp.ifad.dk\/pub\/users\/sten, December 1995.","key":"2_CR1"},{"unstructured":"Michael Barr and Charles Wells. Category Theory for Computing Science. Prentice Hall, 1990.","key":"2_CR2"},{"doi-asserted-by":"crossref","unstructured":"Ilya Beylin and Peter Dybjer. Extracting a proof of coherence for monoidal categories from a formal proof of normalization for monoids. In Stefano Berardi and Mario Coppo, editors, TYPES\u2019 95, LNCS, 1996. To appear.","key":"2_CR3","DOI":"10.1007\/3-540-61780-9_61"},{"unstructured":"J. Camilleri and T. Melham. Reasoning with inductively defined relations in the HOL theorem prover. Technical Report No. 265, University of Cambridge Computer Laboratory, August 1992.","key":"2_CR4"},{"unstructured":"Thierry Coquand. Pattern matching with dependent types. In Proceedings of The 1992 Workshop on Types for Proofs and Programs, June 1992.","key":"2_CR5"},{"key":"2_CR6","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P. Dybjer","year":"1994","unstructured":"Peter Dybjer. Inductive families. Formal Aspects of Computing, 6:440\u2013465, 1994.","journal-title":"Formal Aspects of Computing"},{"unstructured":"M. J. C. Gordon. HOL: A proof generating system for higher order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving. Springer-Verlag, 1989.","key":"2_CR7"},{"unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theoremproving Environment for Higher-Order Logic. Cambridge University Press, 1993.","key":"2_CR8"},{"doi-asserted-by":"crossref","unstructured":"E. Gunter. A broader class of trees for recursive type definition for HOL. In J. J. Joyce and C. H. Seger, editors, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, volume 780 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","key":"2_CR9","DOI":"10.1007\/3-540-57826-9_131"},{"unstructured":"G\u00e9rard Huet and Amokrane Saibi. Constructive category theory. In Proceedings of the Joint CLICS-TYPES Workshop on Categories and Type Theory, G\u00f6teborg, January 1995.","key":"2_CR10"},{"key":"2_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-9839-7","volume-title":"Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics","author":"S. M. Lane","year":"1971","unstructured":"Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, 1971."},{"unstructured":"Lena Magnusson. The Implementation of ALF \u2014 a Proof Editor for Martin-L\u00f6f's Monomorphic Type Theory with Explicit Substitution. PhD thesis, Chalmers T. H., 1994.","key":"2_CR12"},{"doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. An intuitionistic theory of types: Predicative part. In Logic Colloquium\u2019 73, pages 73\u2013118. North-Holland, 1975.","key":"2_CR13","DOI":"10.1016\/S0049-237X(08)71945-1"},{"doi-asserted-by":"crossref","unstructured":"Per Martin-L\u00f6f. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science, 1979, pages 153\u2013175. North-Holland, 1982.","key":"2_CR14","DOI":"10.1016\/S0049-237X(09)70189-2"},{"unstructured":"Per Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984.","key":"2_CR15"},{"unstructured":"T. Melham. A package for inductive relation definition in HOL. In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windly, editors, Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, August 1991. IEEE Computer Society Press, 1992.","key":"2_CR16"},{"unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan Smith. Programming in Martin-L\u00f6f's Type Theory: an Introduction. Oxford University Press, 1990.","key":"2_CR17"},{"doi-asserted-by":"crossref","unstructured":"L. C. Paulson. A higher order implementation of rewriting. Science of Computer Programming, 3, 1983.","key":"2_CR18","DOI":"10.1016\/0167-6423(83)90008-4"},{"doi-asserted-by":"crossref","unstructured":"B. Pierce. Basic Category Theory for Computer Scientists. MIT Press, 1991.","key":"2_CR19","DOI":"10.7551\/mitpress\/1524.001.0001"},{"doi-asserted-by":"crossref","unstructured":"D. Syme. A new interface for HOL \u2014 ideas, issues and implementation. In E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors, Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, volume 971 of Lecture Notes in Computer Science. Springer-Verlag, 1995.","key":"2_CR20","DOI":"10.1007\/3-540-60275-5_74"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0105394","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,19]],"date-time":"2019-06-19T05:44:34Z","timestamp":1560923074000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105394"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0105394","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}