{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:23Z","timestamp":1761611123117},"reference-count":21,"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)00107-0","type":"journal-article","created":{"date-parts":[[2004,2,5]],"date-time":"2004-02-05T10:34:35Z","timestamp":1075977275000},"page":"111-127","source":"Crossref","is-referenced-by-count":4,"title":["Tripos Theory in Retrospect"],"prefix":"10.1016","volume":"23","author":[{"given":"Andrew M.","family":"Pitts","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB1","doi-asserted-by":"crossref","unstructured":"Awodey S., L. Birkedal, and D.S. Scott (1999). Local realizability toposes and a modal logic for computability. In this volume.","DOI":"10.1016\/S1571-0661(04)00101-X"},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB2","doi-asserted-by":"crossref","unstructured":"Fourman, M. P. and D. S. Scott (1979). Sheaves and logic. In M. P. fourman, C. J. Mulvey, and D. S. Scott, (Eds.), Applications of Sheaves, Proceedings, Durham 1977, Volume 753 of Lecture Notes in Mathematics, pp. 302\u2013401 springer-Verlag, Berlin.","DOI":"10.1007\/BFb0061824"},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB3","doi-asserted-by":"crossref","unstructured":"Hofmann M. (1999). Semantical analysis of higher-order abstract syntax. In 14th annual Symposium on Logic in Computer Science, IEEE Computer Society Press, Washington.","DOI":"10.1109\/LICS.1999.782616"},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB4","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0168-0072(88)90018-8","article-title":"A small complete category","volume":"40","author":"Hyland","year":"1982","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB5","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1017\/S0305004100057534","article-title":"Tripos theory","volume":"88","author":"Hyland","year":"1980","journal-title":"Math. Proc. Cambridge Philos. Soc"},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB6","series-title":"Number 10 in LMS Mathematical Monographs","article-title":"Topos Theory","author":"Johnstone","year":"1997"},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB7","unstructured":"P. T. Johnstone, and R. Par\u00e9 (Eds.) (1978). Indexed Categories and Their Applications, Volume 661 of Lecture Notes in Mathematics. Springer-Verlag, Berlin."},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB8","doi-asserted-by":"crossref","first-page":"109","DOI":"10.2307\/2269016","article-title":"On the interpretation of intuitionistic number theory","volume":"10","author":"Kleene","year":"1945","journal-title":"Journal of sumbolic Logic"},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB9","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1111\/j.1746-8361.1969.tb01194.x","article-title":"Adjointness in foundations","volume":"23","author":"Lawvere","year":"1969","journal-title":"Dialectica"},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB10","series-title":"Applications of Categorical Algebra","first-page":"1","article-title":"Equality in hyperdoctrines and the comprehension scema as an adjoint functor","author":"Lawvere","year":"1970"},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB11","unstructured":"Longley J. (1995). Realizability Toposes and Language Semantics. Ph. D. thesis, Edinburgh University."},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB12","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1305\/ndjfl\/1093634727","article-title":"The fibrational formulation of intuitionistic predicate logic. I: Completeness according to G\u00f6del, Kripke, and L\u00e4ichli","volume":"34","author":"Makkai","year":"1993","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB13","unstructured":"Makkai M. and G. E. Reyes (1977). First Order Categorical Logic, Volume 611 of Lecture Notes in Mathematics. Springer-Verlag, Berlin."},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB14","unstructured":"Phoa W. (1990). Domain Theory in Realizability Toposes. Ph.D. thesis, Cambridge University."},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB15","unstructured":"Pitts, A. M. (1981. The Theory of Triposes. Ph. D. thesis, Cambridge University."},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB16","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1016\/0168-0072(89)90007-9","article-title":"Conceptual completeness for first order intuitionistic logic: an application of categorical logic","volume":"41","author":"Pitts","year":"1989","journal-title":"Annals pure Applied Logic"},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB17","doi-asserted-by":"crossref","first-page":"33","DOI":"10.2307\/2275175","article-title":"On an interpretation of second order quantification in first order intuitionistic propositional logic","volume":"57","author":"Pitts","year":"1992","journal-title":"Jour. Symbolic Logic"},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB18","unstructured":"Pitts, A. M. (1995). Categorical logic. Technical Report 367, Cambridge University Computer Laboratory. To appear as a chapter of Handbook of Logic in Computer Science, Vol. V (Oxford University Press)."},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB19","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1017\/S096012959900273X","article-title":"General synthetic domain theory\u2013-a logical approach","volume":"9","author":"Reus","year":"1999","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB20","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1142\/S0129054190000242","article-title":"About modest sets","volume":"1","author":"Rosolini","year":"1990","journal-title":"International Journal of Foundations of Computer Science"},{"key":"10.1016\/S1571-0661(04)00107-0_NEWBIB21","unstructured":"van Oosten J. (1991). Exercises in Realizability. Ph.D. thesis, Universiteit van Amsterdam."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001070?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001070?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,15]],"date-time":"2019-02-15T06:56:54Z","timestamp":1550213814000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104001070"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999]]}},"alternative-id":["S1571066104001070"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00107-0","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}