{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:28:17Z","timestamp":1725474497536},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651376"},{"type":"electronic","value":"9783540495628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0097788","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T09:27:48Z","timestamp":1164360468000},"page":"88-111","source":"Crossref","is-referenced-by-count":0,"title":["A type-free formalization of mathematics where proofs are objects"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Dowek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,26]]},"reference":[{"issue":"3","key":"6_CR1","doi-asserted-by":"publisher","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"P.B. Andrews","year":"1971","unstructured":"P.B. Andrews, Resolution in type theory, The Journal of Symbolic Logic, 36, 3 (1971) pp. 414\u2013432.","journal-title":"The Journal of Symbolic Logic"},{"doi-asserted-by":"crossref","unstructured":"M.J. Beeson, Foundations of Constructive Mathematics, Springer-Verlag (1985).","key":"6_CR2","DOI":"10.1007\/978-3-642-68952-9"},{"doi-asserted-by":"crossref","unstructured":"G. Boolos, The logic of provability, Cambridge University Press (1993).","key":"6_CR3","DOI":"10.1017\/CBO9780511625183"},{"unstructured":"N.G. de Bruijn, A Survey of the project automath, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.R. Hindley, J.P. Seldin (Eds.), Academic Press (1980).","key":"6_CR4"},{"key":"6_CR5","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church, A formulation of the simple theory of types. The Journal of Symbolic Logic, 5 (1940) pp. 56\u201368.","journal-title":"The Journal of Symbolic Logic"},{"unstructured":"Th. Coquand, An analysis of Girard's paradox, Rapport de Recherche 531, Institut National de Recherche en Informatique et en Automatique (1986).","key":"6_CR6"},{"unstructured":"Th. Coquand, A new paradox in type theory, Logic, Methodology and Philosophy of Science IX, D. Prawitz, B. Skyrms and D. Westerst\u00e5hl (Ed.), Elsevier (1994) pp. 555\u2013570.","key":"6_CR7"},{"key":"6_CR8","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Th. Coquand, G. Huet, The calculus of constructions, Information and Computation, 76 (1988) pp. 95\u2013120.","journal-title":"Information and Computation"},{"issue":"2","key":"6_CR9","doi-asserted-by":"publisher","first-page":"49","DOI":"10.2307\/2266302","volume":"7","author":"H.B. Curry","year":"1942","unstructured":"H.B. Curry, The combinatory foundations of mathematical logic, The Journal of Symbolic Logic, 7, 2, (1942) pp. 49\u201364.","journal-title":"The Journal of Symbolic Logic"},{"key":"6_CR10","volume-title":"Combinatory logic, Vol. 1","author":"H.B. Curry","year":"1958","unstructured":"H.B. Curry, R. Feys, Combinatory logic, Vol. 1, North Holland, Amsterdam (1958)."},{"key":"6_CR11","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/BFb0014051","volume":"902","author":"G. Dowek","year":"1995","unstructured":"G. Dowek, Lambda-calculus, combinators and the comprehension scheme, Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 902 (1995) pp. 154\u2013170. Rapport de Recherche 2565, Institut National de Recherche en Informatique et en Automatique (1995).","journal-title":"Lecture Notes in Computer Science"},{"unstructured":"G. Dowek, Collections, types and sets, Rapport de Recherche 2708, Institut National de Recherche en Informatique et en Automatique (1995). Mathematical Structures in Computer Science (to appear).","key":"6_CR12"},{"unstructured":"G. Dowek, A type-free formalization of mathematics where proofs are objects Rapport de Recherche 2915, Institut National de Recherche en Informatique et en Automatique (1996).","key":"6_CR13"},{"doi-asserted-by":"crossref","unstructured":"S. Feferman, Finitary inductively presented logics, Logic Colloquium '88, R. Ferro, C. Bonotto, S. Valentini and A. Zanardo (Ed.), North Holland (1989).","key":"6_CR14","DOI":"10.1016\/S0049-237X(08)70270-2"},{"issue":"1","key":"6_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2274902","volume":"56","author":"S. Feferman","year":"1991","unstructured":"S. Feferman, Reflecting on incompleteness, The Journal of Symbolic Logic, 56, 1, (1991) pp. 1\u201349.","journal-title":"The Journal of Symbolic Logic"},{"unstructured":"J.Y. Girard, Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieur, Th\u00e8se de Doctorat d'\u00c9tat, Universit\u00e9 de Paris 7 (1972).","key":"6_CR16"},{"unstructured":"K. G\u00f6del, An interpretation of the intuitionistic propositional calculus, 1933, in K. G\u00f6del collected works, S. Feferman, J.W. Dawson Jr., S.C. Kleene G.H. Moore, R.M. Solovay, J. van Heijenoort (Ed.), Oxford University Press (1986).","key":"6_CR17"},{"issue":"3","key":"6_CR18","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1305\/ndjfl\/1040511340","volume":"35","author":"V. Halbach","year":"1994","unstructured":"V. Halbach, A system of complete and consistent truth, Notre Dame Journal of Formal Logic, 35, 3 (1994) pp. 311\u2013327.","journal-title":"Notre Dame Journal of Formal Logic"},{"unstructured":"W. A. Howard, The Formul\u00e6-as-type notion of construction, 1969, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.R. Hindley, J.P. Seldin (Ed.), Academic Press (1980).","key":"6_CR19"},{"unstructured":"G. Huet, personal communication.","key":"6_CR20"},{"key":"6_CR21","first-page":"149","volume":"26","author":"J.L. Krivine","year":"1990","unstructured":"J.L. Krivine, M. Parigot, Programming with proofs, J. Inf. Process. Cybern. EIK 26 (1990) pp. 149\u2013167.","journal-title":"J. Inf. Process. Cybern. EIK"},{"key":"6_CR22","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/BF00649483","volume":"14","author":"V. McGee","year":"1985","unstructured":"V. McGee, How truthlike can a predicate be? A negative result, Journal of Philosophical Logic 14 (1985) pp. 399\u2013410.","journal-title":"Journal of Philosophical Logic"},{"unstructured":"P. Martin-L\u00f6f Constructive mathematics and computer programming, Logic, Methodology and Philosophy of Science VI, 1979, L.J. Cohen, J. \u0141o\u015b, H. Pfeiffer, K.-P. Podewski (Ed.), North-Holland (1982) pp. 153\u2013175.","key":"6_CR23"},{"unstructured":"P. Martin-L\u00f6f, Intuitionistic type theory, Bibliopolis, Napoli (1984).","key":"6_CR24"},{"key":"6_CR25","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0037116","volume":"664","author":"C. Paulin-Mohring","year":"1993","unstructured":"Ch. Paulin-Mohring, Inductive definitions in the system COQ, Rules and properties, Typed Lambda Calculi and Applications, Lecture Notes in Computer Science 664 (1993) pp. 328\u2013345.","journal-title":"Lecture Notes in Computer Science"},{"key":"6_CR26","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1016\/S0747-7171(06)80007-6","volume":"15","author":"C. Paulin-Mohring","year":"1993","unstructured":"Ch. Paulin-Mohring, B. Werner, Synthesis of ML programs in the system Coq, Journal of Symbolic Computation, 15, 5\u20136 (1993) pp. 607\u2013640.","journal-title":"Journal of Symbolic Computation"},{"key":"6_CR27","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"G. Plotkin. Building-in equational theories, Machine Intelligence, 7 (1972) pp. 73\u201390.","journal-title":"Machine Intelligence"},{"doi-asserted-by":"crossref","unstructured":"W. W. Tait, Infinitely long terms of transfinite type, Formal Systems and Recusrive Functions, J.N. Crossley, M. Dummett (Ed.), North-Holland (1965).","key":"6_CR28","DOI":"10.1016\/S0049-237X(08)71689-6"},{"unstructured":"A.N. Whitehead, B. Russell, Principia mathematica, Cambridge University Press (1910\u20131913, 1925\u20131927).","key":"6_CR29"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0097788","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,22]],"date-time":"2019-04-22T10:54:11Z","timestamp":1555930451000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0097788"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651376","9783540495628"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/bfb0097788","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}