{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T06:49:09Z","timestamp":1760078949405},"reference-count":44,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":5323,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[1999]]},"DOI":"10.1016\/s1571-0661(04)00108-2","type":"journal-article","created":{"date-parts":[[2004,2,5]],"date-time":"2004-02-05T10:34:35Z","timestamp":1075977275000},"page":"128-158","source":"Crossref","is-referenced-by-count":5,"title":["Realizability Models for Type Theories"],"prefix":"10.1016","volume":"23","author":[{"given":"Bernhard","family":"Reus","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB1","series-title":"A Theory of Objects","author":"Abadi","year":"1996"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB2","doi-asserted-by":"crossref","unstructured":"M. Abadi and G.D. Plotkin. A per model of polymorphism and recursive types. In J. Mitchell, editor, 5th Annual IEEE Symposium on Logic in Computer Science, pages 355\u2013365, Philadelphia, 1990. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1990.113761"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB3","unstructured":"T. Altenkirch. Constructions, Inductive Types and Strong Normalization. PhD thesis, University of Edinbugh, 1993. Available as report ECS-LFCS-93\u2013279."},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB4","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90074-C","article-title":"Recursion over realizability structures","volume":"91","author":"Amadio","year":"1991","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB5","series-title":"Cambridge Tracts in Theoretical Computer Science","article-title":"Domains and Lambda-Calculi","author":"Amadio","year":"1998"},{"issue":"2","key":"10.1016\/S1571-0661(04)00108-2_NEWBIB6","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","article-title":"Introduction to generalized type systems","volume":"1","author":"Barendregt","year":"1991","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB7","series-title":"Foundations of constructive mathematics","author":"Beeson","year":"1985"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB8","doi-asserted-by":"crossref","unstructured":"L. Birkedal, A. Carboni, G. Rosolini, and D.S. Scott. Type theory via exact categories. In Proceedings of the 13th Annual IEEE Symposium on Logic in computer Science, pages 188\u2013198, Indianapolis, Indiana, June 1998. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1998.705655"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB9","doi-asserted-by":"crossref","unstructured":"K. Bruce and J.C. Mitchell. Per models of subtyping, recursive types and higher-order polymorphism. In Proc. 19th ACM Symp. on Principles of Programming, pages 316\u2013327, 1992.","DOI":"10.1145\/143165.143230"},{"issue":"4","key":"10.1016\/S1571-0661(04)00108-2_NEWBIB10","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1017\/S0956796800000198","article-title":"A Semantic Basis for Quest","volume":"1","author":"Cardelli","year":"1991","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB11","unstructured":"Th. Coquand. An analysis of girard's paradox. In 1st Symp. on Logic in Computer Science, Washington, 1986. IEEE Computer Soc. Press."},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB12","doi-asserted-by":"crossref","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB13","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1007\/BF01211308","article-title":"Inductive families","volume":"6","author":"Dybjer","year":"1994","journal-title":"formal Aspects of Computing"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB14","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/S0022-4049(96)00164-8","article-title":"Two models of synthetic domain theory","volume":"116","author":"Fiore","year":"1997","journal-title":"Journal of Pure and Applied Algebra"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB15","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/0890-5401(92)90019-C","article-title":"Extensional PERs","volume":"98","author":"Freyd","year":"1992","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB16","unstructured":"J.-Y. Grard, Y. lafont, and P. Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Presss, 1989."},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB17","doi-asserted-by":"crossref","unstructured":"M. Hofmann. Syntax and semantics of dependent types. In Semantic and Logic of Computation. Cambridge University Press, 1997.","DOI":"10.1017\/CBO9780511526619.004"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB18","doi-asserted-by":"crossref","unstructured":"J.M.E. Hyland. The effective topos. In a.S. Troelstra and D. Van Dalen, editors, The L.E.J. Brouwer Centenary Symposium, pages 165\u2013216. North Holland Publishing Company, 1982.","DOI":"10.1016\/S0049-237X(09)70129-6"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB19","doi-asserted-by":"crossref","unstructured":"J.M.E. Hyland. First steps in synthetic domain theory. In A. Carboni, M.C. Pediccho, and G. Rosolini, editors, Category Theory'90, volume 1144 of Lectures Notes in Mathematics, pages 131\u2013156, Como, 1992. Springer-Verlag.","DOI":"10.1007\/BFb0084217"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB20","series-title":"Categorical Logic and Type Theory","author":"Jocobs","year":"1999"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB21","unstructured":"J.R. Longley. Realizability Toposes and Language Semantics. PhD thesis, Edinbugh, 1995."},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB22","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1017\/S0960129597002387","article-title":"A uniform approach to domain theory in realizability models","volume":"7","author":"Longley","year":"1997","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB23","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1017\/S0960129500001298","article-title":"Constructive natural deduction and its \u03c9-set interpretation","volume":"1","author":"Longo","year":"1991","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB24","doi-asserted-by":"crossref","unstructured":"Z. Luo. Computation and Reasoning - A type Theory for Computer Science, volume 11 of Monographs on computer Science. Oxford University Press, 1994.","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB25","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f. An intitionisitc theory of types, predicative part. In Logic Colloquium 1973, pages 73\u2013118, 1975.","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB26","first-page":"73","article-title":"An intuitionisitc theory of types, predicative part","author":"Martin-L\u00f6f","year":"1975","journal-title":"Logic Colloquium 1973"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB27","series-title":"Intuitionistic Type Theory. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB28","series-title":"The Definition of Standard ML","author":"Milner","year":"1990"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB29","series-title":"foundations of Programming Languages","author":"Mitchell","year":"1996"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB30","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J.M. Smith. Programming in Martin L\u00f6f's Type Theory, volume 7 of Monograps on Computer Science. Oxford University Press, 1990."},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB31","unstructured":"W.K.-S. Phoa. Domain Theory in Realizability Toposes. PhD thesis, Cambridge, 1990."},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB32","unstructured":"W.K.-S. Phoa. An introduction to fibrations, topos theory, the effective topos and modest sets. Technical Report EXS-LFCS-92\u2013208, Department of Computer Science, University of Edinbugh, 1992."},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB33","unstructured":"B. Reus. Program Verification in Synthetic Domain Theory. Dodt. Diss., Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, 1995. Shaker Verlag, Aachen."},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB34","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1023\/A:1008600521659","article-title":"Extensional \u03a3-spaces in type theory","volume":"7","author":"Reus","year":"1999","journal-title":"Applied Categorical Structures"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB35","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1017\/S096012959900273X","article-title":"General Synthetic Domain Theory - a logical approach","volume":"9","author":"Reus","year":"1999","journal-title":"Math. Struct. in Comp. Sci"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB36","unstructured":"G. Rosolini. Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford, 1986."},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB37","doi-asserted-by":"crossref","unstructured":"G. Rosolini. Categories and effective computations. In D.H. Pitt, A. Poign\u00e9, and D.E. Rydeheard, editors, Category theory and Computer Science, volume 283 of Lectures Notes in Computer Science, pages 1\u201311, Edinburgh, 1987. Springer-Verlag.","DOI":"10.1007\/3-540-18508-9_17"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB38","first-page":"436","article-title":"An ExPer model for Quest","volume":"volume 598","author":"Rosolini","year":"1991"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB39","unstructured":"D.S. Scott. A new category? Domains, spaces and equivalence relations. Manuscript, 1996."},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB40","series-title":"Semantics of Type Theory, Correctness, Completeness and Independence Results","author":"Streicher","year":"1991"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB41","first-page":"29","article-title":"Dependence and independence results for (impredicative) calculi of dependent types","volume":"2","author":"Streicher","year":"1992","journal-title":"MSCS"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB42","series-title":"6th Symp. on Logic in Computer Science","first-page":"152","article-title":"The fixed point property in synthetic domain theory","author":"Taylor","year":"1991"},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB43","unstructured":"P. Taylor. Practical Foundations of Mathematics, volume 59 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999."},{"key":"10.1016\/S1571-0661(04)00108-2_NEWBIB44","unstructured":"J. van Oosten and A.K. Simpson Axioms and (Counter-)examples in Synthetic Domain Theory. Jour. Pure and Applied Logic, to appear, 1999."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001082?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001082?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,1,12]],"date-time":"2024-01-12T11:27:23Z","timestamp":1705058843000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104001082"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999]]}},"alternative-id":["S1571066104001082"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00108-2","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}