{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T02:13:54Z","timestamp":1778292834286,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540190271","type":"print"},{"value":"9783540389415","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/3-540-19027-9_10","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T19:55:59Z","timestamp":1330199759000},"page":"145-159","source":"Crossref","is-referenced-by-count":22,"title":["Programming with proofs: A second order type theory"],"prefix":"10.1007","author":[{"given":"Michel","family":"Parigot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"10_CR1","unstructured":"H.P. BARENDREGT, The Lambda Calculus, Studies in Logic, North-Holland, 1981."},{"key":"10_CR2","unstructured":"N. DE BRUIJN, A survey of the project Automath, to H.B. CURRY: essays on combinatory logic, \u03bb-calculus and formalism, Seldin\/Hindley (eds), pp 579\u2013606, Academic Press, 1980."},{"key":"10_CR3","unstructured":"T. COQUAND, Une th\u00e9orie des constructions, Th\u00e8se de 3eme cycle, Universit\u00e9 Paris 7, 1985."},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"T. COQUAND, G. HUET, Constructions: a higher order proof system for mechanizing mathematics, Proc. EUROCAL 85, LNCS 203.","DOI":"10.1007\/3-540-15983-5_13"},{"key":"10_CR5","unstructured":"R.L. CONSTABLE et. al., Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986."},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"G. COUSINEAU, P. L. CURIEN, M. MAUNY, The categorical abstract machine, LNCS 201, 1985.","DOI":"10.1007\/3-540-15975-4_29"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"J.Y. GIRARD, Une extension de l'interpr\u00e9tation de G\u00f6del \u00e0 l'analyse, et son application \u00e0l'\u00e9limination des coupures dans l'analyse et dans la th\u00e9orie des types, Proc. 2nd Scandinavian Logic Symp., pp 63\u201392, North-Holland, 1970.","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"10_CR8","unstructured":"J.Y. GIRARD, Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur, Th\u00e8se d'\u00e9tat, Universit\u00e9 Paris 7, 1972."},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"J.Y. GIRARD, The System F of variable types, fifteen years later, Theoretical Computer Science, 1987.","DOI":"10.1016\/0304-3975(86)90044-7"},{"key":"10_CR10","unstructured":"W.A. HOWARD, The formulae as types notion of construction, manuscript, 1969 (published in Seldin\/Hindley (eds), To H.B. CURRY; essays on combinatory logic, \u03bb-calculus and formalism, pp. 479\u2013490, Academic Press, 1980)."},{"key":"10_CR11","unstructured":"J.L. KRIVINE, Programmation en Arithmetique Fonctionnelle du Second Ordre, manuscript."},{"key":"10_CR12","unstructured":"J.L. KRIVINE, Un algorithme non typable dans le syst\u00e8me F, CRAS, 1987."},{"key":"10_CR13","unstructured":"J.L. KRIVINE, M. PARIGOT, Programming with proofs, preprint, presented at 6th Symposium on Computation Theory, Wendisch-Rietz, November 1987."},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"H. LAUCHLI, An abstract notion of realizability for which intuitionistic predicate calculus is complete, in Kino\/Myhill\/vesley (eds), Intuitionism and proof theory, pp 227\u2013234, North-Holland, 1970.","DOI":"10.1016\/S0049-237X(08)70754-7"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"P. MARTIN-LOF, Constructive Mathematics and Computer programming, Proc. 6th Cong. Logic, Methodology and Philosophy of Science, pp 153\u2013175, North-Holland, 1982.","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"10_CR16","unstructured":"P. MARTIN-LOF, Intuitionistic type theory, Bibliopolis, 1984."},{"key":"10_CR17","unstructured":"M. PARIGOT, Preuves et programmes: les math\u00e9matiques comme langage de programmation, Images des Math\u00e9matiques, Courrier du CNRS (\u00e0 para\u00eetre)."},{"key":"10_CR18","unstructured":"M. PARIGOT, Recursive programming with proofs, preprint, december 1987."},{"key":"10_CR19","first-page":"97","volume":"185","author":"J.R. Reynolds","year":"1985","unstructured":"J.R. REYNOLDS, Three approaches to type structure, LNCS 185, 1985, pp 97\u2013138.","journal-title":"LNCS"}],"container-title":["Lecture Notes in Computer Science","ESOP '88"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-19027-9_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:16:09Z","timestamp":1605644169000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-19027-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540190271","9783540389415"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-19027-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1988]]}}}