{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:20:42Z","timestamp":1725456042778},"publisher-location":"Berlin\/Heidelberg","reference-count":17,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354051662X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0018354","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T07:50:09Z","timestamp":1132645809000},"page":"213-223","source":"Crossref","is-referenced-by-count":4,"title":["Dictoses"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Ehrhard","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"crossref","first-page":"10","DOI":"10.2307\/2273784","volume":"50","author":"J. B\u00e9nabou","year":"1985","unstructured":"J. B\u00e9nabou \u201cFibered categories and the foundation of naive category theory\u201d J. of Symbolic Logic 50(1985) 10\u201337.","journal-title":"J. of Symbolic Logic"},{"doi-asserted-by":"crossref","unstructured":"T. Ehrhard \u201cA categorical semantics of constructions\u201d Logic in Computer Science 1988.","key":"14_CR2","DOI":"10.1109\/LICS.1988.5125"},{"unstructured":"T. Ehrhard \u201cUne s\u00e9mantique cat\u00e9gorique des types d\u00e9pendants. Application au Calcul des Constructions.\u201d Th\u00e8se, Paris VII, 1988.","key":"14_CR3"},{"doi-asserted-by":"crossref","unstructured":"M. Hyland \u201cThe effective topos\u201d in The L.E.J. Brouwer Centenary Symposium (ed. Troelstra et Van Dalen), North Holland (1982), 165\u2013216.","key":"14_CR4","DOI":"10.1016\/S0049-237X(09)70129-6"},{"unstructured":"M. Hyland \u201cA small complete category\u201d Conference \u201cChurch's Thesis 50 years later\u201d Zeiss (NL) 1986. Ann. Pure and Appl. Logic, \u00e0 para\u00eetre.","key":"14_CR5"},{"doi-asserted-by":"crossref","unstructured":"M. Hyland et A. Pitts \u201cTheory of constructions: categorical semantics and topos-theoretic models\u201d to appear in the proceedings of the conference Category in Computer Science and Logic, Contemporary Mathematics, AMS (1988).","key":"14_CR6","DOI":"10.1090\/conm\/092\/1003199"},{"unstructured":"M. Hyland, E.P. Robinson et G. Rossolini \u201cThe discrete objects in the Effective Topos\u201d To appear.","key":"14_CR7"},{"unstructured":"P.T. Johnstone \u201cTopos Theory\u201d Academic Press, Inc.","key":"14_CR8"},{"unstructured":"J. Lambek and P.J. Scott \u201cIntroduction to higher order categorical logic\u201d Cambridge studies in advanced mathematics. Cambridge University Press (1986).","key":"14_CR9"},{"unstructured":"P. Martin L\u00f6f \u201cIntuisionistic type theory\u201d Bibliopolis 1985","key":"14_CR10"},{"unstructured":"A. Pitts \u201cTripos theory.\u201d Ph. D. Thesis.","key":"14_CR11"},{"doi-asserted-by":"crossref","unstructured":"A. Pitts \u201cPolymorphism is set-theoretic... constructively.\u201d proceedings de la conf\u00e9rence \u201cCategory theory and computer science\u201d Edinburgh 1987. LNCS.","key":"14_CR12","DOI":"10.1007\/3-540-18508-9_18"},{"unstructured":"A. Scedrov \u201cRecursive realazibility semantics for calculus of constructions\u201d Unpublished.","key":"14_CR13"},{"doi-asserted-by":"crossref","unstructured":"R.A.G. Seely. \u201cHyperdoctrines, natural deduction and the Beck condition\u201d Zeitschrift f\u00fcr Mat. Logik und Grundlagen d. Math. 29 505\u2013542.","key":"14_CR14","DOI":"10.1002\/malq.19830291005"},{"doi-asserted-by":"crossref","unstructured":"R.A.G. Seely. \u201cLocally Cartesian Closed Categories and Type Theory\u201d Math. Proc. Camb. Phil. Soc. 95, (1984).","key":"14_CR15","DOI":"10.1017\/S0305004100061284"},{"doi-asserted-by":"crossref","unstructured":"R.A.G. Seely. \u201cCategorical Semantics for Higher Order Polymorphic Lambda Calculus\u201d Draft (1986).","key":"14_CR16","DOI":"10.2307\/2273831"},{"unstructured":"T. Streicher \u201cCorrectness and completeness of a semantics of the calculus of constructions with respect to interpretation in doctrines of constructions\u201d Ph.D. Thesis, Passau (1988).","key":"14_CR17"}],"container-title":["Lecture Notes in Computer Science","Category Theory and Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0018354.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,20]],"date-time":"2021-07-20T03:51:23Z","timestamp":1626753083000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0018354"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354051662X"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0018354","relation":{},"subject":[]}}