{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T05:57:27Z","timestamp":1781762247482,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540744634","type":"print"},{"value":"9783540744641","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74464-1_16","type":"book-chapter","created":{"date-parts":[[2007,9,12]],"date-time":"2007-09-12T06:58:12Z","timestamp":1189580292000},"page":"237-252","source":"Crossref","is-referenced-by-count":31,"title":["Subset Coercions in Coq"],"prefix":"10.1007","author":[{"given":"Matthieu","family":"Sozeau","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Springer, Heidelberg (2004)"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/978-3-540-44616-3_3","volume-title":"Recent Trends in Algebraic Development Techniques","author":"N. Shankar","year":"2000","unstructured":"Shankar, N., Owre, S.: Principles and pragmatics of subtyping in PVS. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol.\u00a01827, pp. 37\u201352. Springer, Heidelberg (2000)"},{"key":"16_CR3","unstructured":"Owre, S., Shankar, N.: The formal semantics of PVS. Technical Report SRI-CSL-97-2, Computer Science Laboratory, SRI International, Menlo Park, CA (1997)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/3-540-60117-1_20","volume-title":"Mathematics of Program Construction","author":"C. Parent","year":"1995","unstructured":"Parent, C.: Synthesizing proofs from programs in the Calculus of Inductive Constructions. In: M\u00f6ller, B. (ed.) MPC 1995. LNCS, vol.\u00a0947, pp. 351\u2013379. Springer, Heidelberg (1995)"},{"key":"16_CR5","volume-title":"Programming in Martin-L\u00f6f\u2019s Type Theory","author":"B. Nordstr\u00f6m","year":"1990","unstructured":"Nordstr\u00f6m, B., Petersson, K., Smith, J.M.: Programming in Martin-L\u00f6f\u2019s Type Theory. Oxford University Press, Oxford (1990)"},{"key":"16_CR6","volume-title":"Implementing Mathematics with the Nuprl Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, H., Cleaveland, W., Cremer, J., Harper, R., Howe, D.J., Knoblock, T., Mendler, N., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall, Englewood Cliffs (1986)"},{"key":"16_CR7","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The Calculus of Constructions. Inf. Comp.\u00a076, 95\u2013120 (1988)","journal-title":"Inf. Comp."},{"key":"16_CR8","unstructured":"Sozeau, M.: Russell Metatheoretic Study in Coq, experimental development (2006), http:\/\/www.lri.fr\/~sozeau\/research\/russell\/proof.en.html"},{"key":"16_CR9","unstructured":"Chen, G.: Sous-typage, Conversion de Types et \u00c9limination de la Transitivit\u00e9. PhD thesis, Universit\u00e9 Paris VII, Laboratoire d\u2019Informatique de l\u2019\u00c9cole Normale Sup\u00e9rieure, Paris (1998)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","first-page":"276","volume-title":"Computer Science Logic","author":"Z. Luo","year":"1997","unstructured":"Luo, Z.: Coercive subtyping in type theory. In: van Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol.\u00a01258, pp. 276\u2013296. Springer, Heidelberg (1997)"},{"key":"16_CR11","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1017\/S0956796805005770","volume":"16","author":"R. Adams","year":"2006","unstructured":"Adams, R.: Pure Type Systems with Judgemental Equality. Journal of Functional Programming\u00a016, 219\u2013246 (2006)","journal-title":"Journal of Functional Programming"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Werner, B.: On the strength of proof-irrelevant type theories. In: 3rd International Joint Conference on Automated Reasoning (2006)","DOI":"10.1007\/11814771_49"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/3-540-39185-1_14","volume-title":"Types for Proofs and Programs","author":"A. Miquel","year":"2003","unstructured":"Miquel, A., Werner, B.: The not so simple proof-irrelevant model of CC. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 240\u2013258. Springer, Heidelberg (2003)"},{"key":"16_CR14","unstructured":"Sozeau, M.: Coercion par pr\u00e9dicats en Coq. Master\u2019s thesis, Universit\u00e9 Paris VII, LRI, Orsay, extended version - (2005), http:\/\/www.lri.fr\/~sozeau\/research\/russell\/report.pdf"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Augustsson, L.: Cayenne\u2014A language with dependent types. In: ACM SIGPLAN International Conference on Functional Programming (ICFP), Baltimore, Maryland, pp. 239\u2013250 (1998)","DOI":"10.1145\/291251.289451"},{"issue":"1","key":"16_CR16","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1017\/S0956796803004829","volume":"14","author":"C. McBride","year":"2004","unstructured":"McBride, C., McKinna, J.: The view from the left. J. Funct. Program.\u00a014(1), 69\u2013111 (2004)","journal-title":"J. Funct. Program."},{"key":"16_CR17","unstructured":"Xi, H.: Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University, Pittsburgh, Pennsylvania (1998)"}],"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-74464-1_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:30:45Z","timestamp":1619519445000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74464-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540744634","9783540744641"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74464-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}