{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:50:07Z","timestamp":1725511807508},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540680840"},{"type":"electronic","value":"9783540681038"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68103-8_11","type":"book-chapter","created":{"date-parts":[[2008,5,6]],"date-time":"2008-05-06T04:10:07Z","timestamp":1210047007000},"page":"157-172","source":"Crossref","is-referenced-by-count":10,"title":["Working with Mathematical Structures in Type Theory"],"prefix":"10.1007","author":[{"given":"Claudio","family":"Sacerdoti Coen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/BFb0097784","volume-title":"Types for Proofs and Programs","author":"A. Bailey","year":"1998","unstructured":"Bailey, A.: Coercion synthesis in computer implementations of type-theoretic frameworks. In: Gim\u00e9nez, E. (ed.) TYPES 1996. LNCS, vol.\u00a01512, pp. 9\u201327. Springer, Heidelberg (1998)"},{"key":"11_CR2","unstructured":"Bailey, A.: The Machine-Checked Literate Formalisation Of Algebr. In: Type Theory. PhD thesis, University of Manchester (1998)"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Types for Proofs and Programs","author":"G. Barthe","year":"1996","unstructured":"Barthe, G.: Implicit coercions in type systems. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 1\u201315. Springer, Heidelberg (1996)"},{"key":"11_CR4","unstructured":"Betarte, G., Tasistro, A.: Formalization of systems of algebras using dependent record types and subtyping: An example. In: Proceedings of the 7th. Nordic workshop on Programming Theory, Gothenburg (1995)"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Betarte, G., Tasistro, A.: Extension of Martin-L\u00f6f\u2019s type theory with record types and subtyping. In: Twenty-five Years of Constructive Type Theory, Oxford Science Publications (1998)","DOI":"10.1007\/BFb0097801"},{"key":"11_CR6","unstructured":"Chen, G.: Subtyping, Type Conversion and Transitivity Elimination. PhD thesis, University Paris 7 (1998)"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Chen, G.: Coercive subtyping for the calculus of constructions. In: The 30th Annual ACM SIGPLAN - SIGACT Symposium on Principle of Programming Language (POPL) (2003)","DOI":"10.1145\/604131.604145"},{"issue":"1-2","key":"11_CR8","first-page":"113","volume":"65","author":"T. Coquand","year":"2005","unstructured":"Coquand, T., Pollack, R., Takeyama, M.: A logical framework with dependently typed records. Fundamenta Informaticae\u00a065(1-2), 113\u2013134 (2005)","journal-title":"Fundamenta Informaticae"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/978-3-540-27818-4_7","volume-title":"Mathematical Knowledge Management","author":"L. Cruz-Filipe","year":"2004","unstructured":"Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-corn, the constructive coq repository at nijmegen. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 88\u2013103. Springer, Heidelberg (2004)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic\u00a065(2) (2000)","DOI":"10.2307\/2586554"},{"key":"11_CR11","unstructured":"Gonthier, G.: A computer-checked proof of the four-colour theorem. Available at: http:\/\/research.microsoft.com\/~gonthier\/4colproof.pdf"},{"key":"11_CR12","unstructured":"Hedberg, M.: Unpublished proof formalized in lego by T. Kleymann and in coq by B. Barras, http:\/\/coq.inria.fr\/library\/Coq.Logic.Eqdep_dec.html"},{"key":"11_CR13","unstructured":"Luo, Z.: An Extended Calculus of Constructions. PhD thesis, University of Edinburgh (1990)"},{"issue":"1","key":"11_CR14","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1093\/logcom\/9.1.105","volume":"9","author":"Z. Luo","year":"1999","unstructured":"Luo, Z.: Coercive subtyping. J. Logic and Computation\u00a09(1), 105\u2013130 (1999)","journal-title":"J. Logic and Computation"},{"key":"11_CR15","unstructured":"Mu\u00f1oz, C.: A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory, November 1997. PhD thesis, INRIA (1997)"},{"key":"11_CR16","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/s001650200018","volume":"13","author":"R. Pollack","year":"2002","unstructured":"Pollack, R.: Dependently typed records in type theory. Formal Aspects of Computing\u00a013, 386\u2013402 (2002)","journal-title":"Formal Aspects of Computing"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Saibi, A.: Typing algorithm in type theory with inheritance. In: The 24th Annual ACM SIGPLAN - SIGACT Symposium on Principle of Programming Language (POPL) (1997)","DOI":"10.1145\/263699.263742"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68103-8_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:32:49Z","timestamp":1620016369000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68103-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540680840","9783540681038"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68103-8_11","relation":{},"subject":[]}}