{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:30:03Z","timestamp":1767929403404,"version":"3.49.0"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2018,7,28]],"date-time":"2018-07-28T00:00:00Z","timestamp":1532736000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2019,5]]},"DOI":"10.1007\/s00224-018-9879-9","type":"journal-article","created":{"date-parts":[[2018,7,28]],"date-time":"2018-07-28T04:42:02Z","timestamp":1532752922000},"page":"647-665","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["An Adequacy Theorem for Dependent Type Theory"],"prefix":"10.1007","volume":"63","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]},{"given":"Simon","family":"Huber","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,28]]},"reference":[{"key":"9879_CR1","doi-asserted-by":"crossref","unstructured":"Abel, A., Coquand, Th., Dybjer, P.: Normalization by evaluation for martin-l\u00f6f type theory with typed equality judgements. In: Proceedings of LICS \u201907 (2007)","DOI":"10.1109\/LICS.2007.33"},{"issue":"1","key":"9879_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-8(1:29)2012","volume":"8","author":"A Abel","year":"2012","unstructured":"Abel, A., Scherer, G.: On irrelevance and algorithmic equality in predicative type theory. Logical Methods Comput. Sci. 8(1), 1\u201336 (2012)","journal-title":"Logical Methods Comput. Sci."},{"key":"9879_CR3","first-page":"1","volume":"1657","author":"P Aczel","year":"1998","unstructured":"Aczel, P.: On relating type theories and set theories. Types for proofs and programs. LNCS 1657, 1\u201318 (1998)","journal-title":"LNCS"},{"issue":"2","key":"9879_CR4","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. J. Funct. Program. 16(2), 219\u2013246 (2006)","journal-title":"J. Funct. Program."},{"key":"9879_CR5","unstructured":"Cardelli, L.: A polymorphic \u03bb-calulus with type:type. SRC Research Report 10 (1986)"},{"key":"9879_CR6","doi-asserted-by":"crossref","unstructured":"Coquand, Th.: An algorithm for testing conversion in type theory. In: Logical Frameworks, pp 255\u2013279 (1991)","DOI":"10.1017\/CBO9780511569807.011"},{"key":"9879_CR7","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0890-5401(89)90068-0","volume":"81","author":"Th Coquand","year":"1989","unstructured":"Coquand, Th., Gunter, C., Winskel, G.: Domain theoretic models of polymorphisms. Inf. Comput. 81, 123\u2013167 (1989)","journal-title":"Inf. Comput."},{"key":"9879_CR8","doi-asserted-by":"crossref","unstructured":"Coquand, Th., Spiwack, A.: A proof of strong normalisation using domain theory. In: Proceeding of LICS \u201906, pp 307\u2013316 (2006)","DOI":"10.1109\/LICS.2006.8"},{"key":"9879_CR9","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/S0049-237X(09)70189-2","volume":"104","author":"P Martin-L\u00f6f","year":"1982","unstructured":"Martin-L\u00f6f, P.: Constructive mathematics and computer programming. Stud. Logic the Found. Math. 104, 153\u2013175 (1982)","journal-title":"Stud. Logic the Found. Math."},{"key":"9879_CR10","volume-title":"Lecture Notes on the Domain Interpretation of Type Theory. Workshop on Semantics of Programming Languages","author":"P Martin-L\u00f6f","year":"1983","unstructured":"Martin-L\u00f6f, P.: Lecture Notes on the Domain Interpretation of Type Theory. Workshop on Semantics of Programming Languages. Chalmers University, G\u00f6teborg (1983)"},{"key":"9879_CR11","unstructured":"Martin-L\u00f6f, P.: Unifying Scott\u2019s Theory of Domains for Denotational Semantics and Intuitionistic Type Theory (Abstract). Atti del Congresso Logica e Filosofia della Scienza San Gimignano, December 1983. Vol. I"},{"key":"9879_CR12","unstructured":"Milne, R.: The formal semantics of computer languages and their implemnetation. PhD thesis, Oxford University Computing Laboratory (1974)"},{"issue":"2","key":"9879_CR13","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0168-0072(90)90044-3","volume":"48","author":"E Palmgren","year":"1990","unstructured":"Palmgren, E., Stoltenberg-Hansen, V.: Domain interpretations of martin-l\u00f6f\u2019s partial type theory. Annals Pure Appl. Logic 48(2), 135\u2013196 (1990)","journal-title":"Annals Pure Appl. Logic"},{"key":"9879_CR14","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/BF01995109","volume":"32","author":"E Palmgren","year":"1992","unstructured":"Palmgren, E., Stoltenberg-Hansen, V.: Remarks on martin-l\u00f6f\u2019s partial type theory. BIT 32, 70\u201382 (1992)","journal-title":"BIT"},{"key":"9879_CR15","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: On the relation between direct and continuation semantics. In: Proceedings of the Second Colloquim on Automata, Languages and Programming, pp 141\u2013156 (1974)","DOI":"10.1007\/978-3-662-21545-6_10"},{"key":"9879_CR16","volume-title":"Proofs and Computations (Perspectives in Logic)","author":"H Schwichtenberg","year":"2012","unstructured":"Schwichtenberg, H., Wainer, S.S.: Proofs and Computations (Perspectives in Logic). Cambridge University Press, Cambridge (2012)"},{"key":"9879_CR17","doi-asserted-by":"crossref","unstructured":"Siles, V., Herbelin, H.: Equality is typable in semi-full pure type systems. In: Proceedings of LICS \u201910 (2010)","DOI":"10.1109\/LICS.2010.19"},{"key":"9879_CR18","doi-asserted-by":"crossref","unstructured":"Scott, D.: Lectures on a mathematical theory of computation. Oxford University PRG Technical Monograph (1981)","DOI":"10.1007\/978-94-009-7893-5_9"},{"key":"9879_CR19","doi-asserted-by":"crossref","unstructured":"Scott, D.: Some ordered sets in computer science. NATO Advanced Study Institutes Series book series (ASIC, vol. 83), pp. 677\u2013718 (1982)","DOI":"10.1007\/978-94-009-7798-3_22"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-018-9879-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-018-9879-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-018-9879-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T02:45:53Z","timestamp":1751769953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-018-9879-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,28]]},"references-count":19,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,5]]}},"alternative-id":["9879"],"URL":"https:\/\/doi.org\/10.1007\/s00224-018-9879-9","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7,28]]},"assertion":[{"value":"28 July 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}