{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:28:07Z","timestamp":1725474487636},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651376"},{"type":"electronic","value":"9783540495628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0097784","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T14:27:48Z","timestamp":1164378468000},"page":"9-27","source":"Crossref","is-referenced-by-count":1,"title":["Coercion synthesis in computer implementations of type-theoretic frameworks"],"prefix":"10.1007","author":[{"given":"Anthony","family":"Bailey","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,26]]},"reference":[{"key":"2_CR1","unstructured":"P. Aczel. Galois: a theory development project. Representation of Mathematics in Logical Frameworks, Turin, 1993."},{"key":"2_CR2","unstructured":"A. Bailey. LEGO with implicit coercions. Draft documenting an earlier version of LEGOwcs. URL:http:\/\/www.cs.man.ac.uk\/~baileya\/LAG\/"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"G. Barthe. Implicit coercions in type systems. Proceedings of TYPES'95, Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61780-9_58"},{"key":"2_CR4","unstructured":"G. Betarte, A. Tasistro. Extension of Martin-L\u00f6f's theory of types with record types and subtyping. Two manuscripts, 1995."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen, T. Coquand, C. Gunter, A. Scedrov. Inheritance as Implicit Coercion. Information and Computation 93, July 1991.","DOI":"10.1016\/0890-5401(91)90055-7"},{"key":"2_CR6","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, J. Fill\u00e2tre, E. Gim\u00e9nez, H. Herbelin, G. Huet, C. Mu\u00f1oz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Sa\u00efbi, B. Werner. The Coq proof assistant reference manual. INRIA-Rocquencourt and CNRS-ENS Lyon, 1996."},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Th. Coquand, G. Huet. The calculus of constructions. Information and Computation 76, 1988.","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"W. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science 13, 1981.","DOI":"10.1016\/0304-3975(81)90040-2"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"A. Jones. Some algorithmic and proof-theoretical aspects of coercive subtyping. Informal Proceedings of TYPES'96 (Aussois), 1997.","DOI":"10.1007\/BFb0097792"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Z. Luo. Computation and reasoning: a type theory for computer science. Oxford University Press, 1994.","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Z. Luo. Coercive subtyping in type theory. Annual Conference of the European Association for Computer Science Logic, Utrecht, 1996.","DOI":"10.1007\/3-540-63172-0_45"},{"key":"2_CR12","unstructured":"Z. Luo, R. Pollack. The LEGO proof development system: user's manual. Technical Report ECS-LFCS-92-211, LFCS, University of Edinburgh, 1992."},{"key":"2_CR13","unstructured":"P. Martin-L\u00f6f. Intuitionistic type theory. Bibliopolis, 1984."},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Higher-order unification, polymorphism, and subsorts. Proceedings of the Second International Workshop on Conditional and Typed Rewriting Systems, LNCS 516, 1990.","DOI":"10.1007\/3-540-54317-1_112"},{"key":"2_CR15","unstructured":"R. Pollack. Implicit syntax. Informal Proceedings of the First Workshop on Logical Frameworks (Antibes), 1990."},{"key":"2_CR16","unstructured":"R. Pollack. How to believe a machine-checked proof. submitted to Twenty-Five Years of Constructive Type Theory: Proceedings of the Venice Meeting URL:ftp:\/\/ftp.dcs.ed.ac.uk\/pub\/lego\/pollack-belief.ps.gz"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"A. Sa\u00efbi. Typing algorithm in type theory with inheritance. 24th Annual SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, 1997.","DOI":"10.1145\/263699.263742"},{"key":"2_CR18","unstructured":"B. Werner. Une th\u00e9orie des constructions inductives. Doctoral thesis, Universit\u00e9 Paris 7, 1994."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0097784","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,8]],"date-time":"2024-02-08T14:06:47Z","timestamp":1707401207000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0097784"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651376","9783540495628"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0097784","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}