{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:11:56Z","timestamp":1761610316283,"version":"build-2065373602"},"reference-count":9,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3831,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,2]]},"DOI":"10.1016\/s1571-0661(04)80490-0","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"53-71","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":5,"title":["Strong Normalization with Singleton Types"],"prefix":"10.1016","volume":"70","author":[{"given":"Judica\u00ebl","family":"Courant","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80490-0_NEWBIB1","unstructured":"David Aspinall. Subtyping with singleton types. In Leszek Pacholski and Jerzy Tiuryn, editors, Proceedings of the 8th Workshop on Computer Science Logic, volume 933 of Lecture Notes in Computer Science, pages 1\u201315, Kazimierz, Poland, September 1994. Springer-Verlag."},{"key":"10.1016\/S1571-0661(04)80490-0_NEWBIB2","unstructured":"Adriana Compagnoni and Healfdene Goguen. Typed operational semantics for higher order subtyping. Technical Report Technical Report ECS-LFCS-97\u2013361, LFCS, University of Edinburgh, July 1997."},{"key":"10.1016\/S1571-0661(04)80490-0_NEWBIB3","article-title":"A meta-mathematical investigation of a Calculus of Constructions","author":"Coquand","year":"1987","journal-title":"Private Communication"},{"key":"10.1016\/S1571-0661(04)80490-0_NEWBIB4","unstructured":"Judica\u00ebl Courant. MC: A module calculus for Pure Type Systems. Research Report 1217, LRI, June 1999."},{"key":"10.1016\/S1571-0661(04)80490-0_NEWBIB5","series-title":"chapter On Girard's Candidats de R\u00e9ductibilit\u00e9","article-title":"Logic and Computer Science","author":"Gallier","year":"1990"},{"key":"10.1016\/S1571-0661(04)80490-0_NEWBIB6","unstructured":"Herman Geuvers. Logics and Type Systems. PhD thesis, University of Nijmegen, September 1993."},{"key":"10.1016\/S1571-0661(04)80490-0_NEWBIB7","unstructured":"Healfdene Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, Aug 1994. LFCS Report ECS-LFCS-94\u2013304."},{"key":"10.1016\/S1571-0661(04)80490-0_NEWBIB8","doi-asserted-by":"crossref","unstructured":"Robert Harper and Christopher Stone. Deciding type equivalence with singleton kinds. In Thomas Reps, editor, Conference Record of the 27th Symposium on Principles of Programming Languages, pages 214\u2013227, Boston, Masschusetts, January 2000. ACM Press.","DOI":"10.1145\/325694.325724"},{"key":"10.1016\/S1571-0661(04)80490-0_NEWBIB9","unstructured":"Masako Takahashi. Parallel reductions in \u03bb-calculus. Technical report, Department of Information Science, Tokyo Institute of Technology, 1993. Internal report."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804900?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804900?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:06:01Z","timestamp":1761609961000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104804900"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,2]]},"references-count":9,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,2]]}},"alternative-id":["S1571066104804900"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80490-0","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2003,2]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Strong Normalization with Singleton Types","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)80490-0","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2003 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}