{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:55:07Z","timestamp":1725663307815},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540171843"},{"type":"electronic","value":"9783540472537"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1986]]},"DOI":"10.1007\/3-540-17184-3_40","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T14:08:43Z","timestamp":1330178923000},"page":"71-84","source":"Crossref","is-referenced-by-count":1,"title":["Sur l'analogie entre les propositions et les types"],"prefix":"10.1007","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,5]]},"reference":[{"issue":"3","key":"4_CR1","doi-asserted-by":"crossref","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"P.B. Andrews","year":"1971","unstructured":"P.B. Andrews. \u201cResolution in Type Theory.\u201d Journal of Symbolic Logic 36,3 (1971), 414\u2013432.","journal-title":"Journal of Symbolic Logic"},{"key":"4_CR2","unstructured":"R. Backhouse. \u201cAlgorithm development in Martin-L\u00f6f's type theory.\u201d University of Essex (July 1984)."},{"key":"4_CR3","unstructured":"H. Barendregt \u201cThe lambda-Calculus: Its Syntax and Semantics.\u201d North-Holland (1980)."},{"key":"4_CR4","volume-title":"Foundations of Constructive Analysis","author":"E. Bishop","year":"1967","unstructured":"E. Bishop. \u201cFoundations of Constructive Analysis\u201d. McGraw-Hill, New-York (1967)."},{"issue":"5","key":"4_CR5","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N.G. Bruijn de","year":"1972","unstructured":"N.G. de Bruijn \u201cLambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem.\u201d Indag. Math. 34,5 (1972), 381\u2013392.","journal-title":"Indag. Math."},{"key":"4_CR6","unstructured":"N.G. de Brujin \u201cA survey of the project Automath.\u201d in Curry Volume, Acc. Press (1980)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"A. Church \u201cA formulation of the simple theory of types\u201d Journal of Symbolic Logic (1940), 56\u201368","DOI":"10.2307\/2266170"},{"key":"4_CR8","unstructured":"R.L. Constable, J.L. Bates. \u201cThe Nearly Ultimate Pearl.\u201d Dept. of Computer Science, Cornell University. (Dec. 1983)."},{"key":"4_CR9","unstructured":"Th. Coquand \u201cUne Theorie des Constructions\u201d Th\u00e8se de 3eme cycle, Paris VII (1985)"},{"key":"4_CR10","unstructured":"Th. Coquand \u201cAn analysis of Girard's Paradox\u201d Submited to the Symposium on Logic and Computer Science, 86"},{"key":"4_CR11","unstructured":"Th. Coquand, G. Huet \u201cConstructions: A Higher Order Proof System for Mechanizing Mathematics.\u201d EUROCAL85, Linz, Springer-Verlag LNCS 203 (1985)."},{"key":"4_CR12","unstructured":"Th. Coquand, G. Huet \u201cConcepts Math\u00e9matiques et Informatiques formalis\u00e9s dans le Calcul des Constructions\u201d Papier presente au Colloque de Logique d'Orsay (1985)"},{"key":"4_CR13","volume-title":"Combinatory Logic Vol. I","author":"H. B. Curry","year":"1958","unstructured":"H. B. Curry, R. Feys. \u201cCombinatory Logic Vol. I.\u201d North-Holland, Amsterdam (1958)."},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"L. Damas, R. Milner. \u201cPrincipal type-schemas for functional programs.\u201d Edinburgh University (1982).","DOI":"10.1145\/582153.582176"},{"key":"4_CR15","unstructured":"J.Y. Girard \u201cInterpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'arithmetique d'ordre sup\u00e9rieur\u201d These d'Etat, Paris VII (1972)"},{"issue":"1","key":"4_CR16","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/322358.322370","volume":"30","author":"S. Fortune","year":"1983","unstructured":"S. Fortune, D. Leivant, M. O'Donnell. \u201cThe Expressiveness of Simple and Second-Order Type Structures.\u201d Journal of the Assoc. for Comp. Mach., 30,1, (Jan. 1983) 151\u2013185.","journal-title":"Journal of the Assoc. for Comp. Mach."},{"key":"4_CR17","unstructured":"Ch. Goad \u201cComputational uses of the manipulation of formal proofs\u201d Ph. D., Stanford University (1980)"},{"key":"4_CR18","doi-asserted-by":"crossref","first-page":"27","DOI":"10.2307\/2964334","volume":"25","author":"R. Harrop","year":"1960","unstructured":"R. Harrop \u201cConcerning formulas of the type A \u21d2 A \u22c1 B, A \u21d2 \u2203x.B(x) in intuitionnistic formal systems\u201d Journal of Symbolic Logic, vol. 25 (1960), 27\u201332","journal-title":"Journal of Symbolic Logic"},{"key":"4_CR19","unstructured":"W. A. Howard. \u201cThe formul\u00e6-as-types notion of construction.\u201d Unpublished manuscript (1969). Reprinted in to H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Eds J. P. Seldin and J. R. Hindley, Academic Press (1980)."},{"key":"4_CR20","unstructured":"S.C. Kleene. \u201cIntroduction to Meta-mathematics.\u201d North Holland (1952)."},{"key":"4_CR21","unstructured":"S.C. Kleene \u201cRealizability: a retrospective survey\u201d L.N. 337, Cambridge Summer School in Mathematical Logic (1971)"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"G. Kreisel. \u201cOn the interpretation of nonfinitist proofs, Part I, II.\u201d JSL 16 (1952, 1953).","DOI":"10.2307\/2267908"},{"key":"4_CR23","unstructured":"J. Lambek. \u201cFrom Lambda-calculus to Cartesian Closed Categories.\u201d in To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, Eds. J. P. Seldin and J. R. Hindley, Academic Press (1980)."},{"key":"4_CR24","unstructured":"P. Martin-L\u00f6f \u201cintuitionistic Type Theory\u201d Bibliopolis, (1980)"},{"key":"4_CR25","unstructured":"A.R. Meyer and J.C. Mitchell \u201cSecond-order Logical Relations\u201d extended abstract (1985)"},{"issue":"3","key":"4_CR26","first-page":"348","volume":"17","author":"R. Milner","year":"1978","unstructured":"R. Milner \u201cA theory of type polymorphism in programming\u201d JCSS 17(3), 348\u2013375 (1978)","journal-title":"JCSS"},{"key":"4_CR27","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/BF01091552","volume":"8","author":"G.C. Mints","year":"1978","unstructured":"G.C. Mints \u201cE-Theorems\u201d J. Soviet Math. 8, 323\u2013329 (1978)","journal-title":"J. Soviet Math."},{"key":"4_CR28","unstructured":"J.C. Mitchell \u201cLambda Calculus Models of Typed Programming langages\u201d Ph. D. thesis, M.I.T. (1984)"},{"key":"4_CR29","unstructured":"C. Mohring. \u201cExemples de D\u00e9veloppement de Programmes dans la Th\u00e9orie des Constructions.\u201d Rapport de DEA, Universit\u00e9 d'Orsay (Sept 85)."},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"J.C. Reynolds \u201cPolymorphism is not Set-Theoretic\u201d Lecture Notes in Computer Science 173, Springer-Verlag, 1984","DOI":"10.1007\/3-540-13346-1_7"},{"key":"4_CR31","unstructured":"B. Russel and A.N. Whitehead \u201cPrincipia Mathematica\u201d Volume 1,2,3 Cambridge University Press (1912)"},{"key":"4_CR32","unstructured":"J.R. Shoenfield \u201cMathematical Logic\u201d Addison-Wesley (1967)"},{"key":"4_CR33","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W. Tait","year":"1967","unstructured":"W. Tait. \u201cIntensional interpretations of functionals of finite type I.\u201d J. of Symbolic Logic 32 (1967) 198\u2013212.","journal-title":"J. of Symbolic Logic"},{"key":"4_CR34","unstructured":"G. Werner \u201cM\u00e9thodes et Probl\u00e8mes de la synth\u00e8se de programmes dans un univers typ\u00e9\u201d Universit\u00e9 de Lille I (1984)"}],"container-title":["Lecture Notes in Computer Science","Combinators and Functional Programming Languages"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-17184-3_40.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:12:28Z","timestamp":1605625948000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-17184-3_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986]]},"ISBN":["9783540171843","9783540472537"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-17184-3_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1986]]}}}