{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:04:19Z","timestamp":1725663859752},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540527534"},{"type":"electronic","value":"9783540471370"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52753-2_47","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:42:18Z","timestamp":1330206138000},"page":"309-321","source":"Crossref","is-referenced-by-count":15,"title":["On the representation of data in lambda-calculus"],"prefix":"10.1007","author":[{"given":"Michel","family":"Parigot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","volume":"39","author":"C. Bohm","year":"1985","unstructured":"C. BOHM, A. BERARDUCCI, Automatic synthesis of typed A\u2014programs on term algebras, TCS 39 (1985), pp 135\u2013154.","journal-title":"TCS"},{"key":"19_CR2","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, Expressiveness of simple and second-order type structures, J.ACM vol 30 (1983), pp 151\u2013185.","journal-title":"J.ACM"},{"key":"19_CR3","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":"19_CR4","unstructured":"J.L. KRIVINE, Un algorithme non typable dans le systeme F, CRAS 1987."},{"key":"19_CR5","unstructured":"J.L. KRIVINE, M. PARIGOT Programming with proofs, FCT 87, Berlin 1987, (to appear in EIK 1990)."},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"D. LEIVANT, Reasoning about functional programs and complexity classes associated with type disciplines, FOCS, 1983, pp 460\u2013469.","DOI":"10.1109\/SFCS.1983.50"},{"key":"19_CR7","unstructured":"P. MARTIN-L\u00d8F, Intuitionistic type theory, Bibliopolis, 1984."},{"key":"19_CR8","unstructured":"P. MALACARIA, personal communcation."},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"M. PARIGOT, Programming with proofs: a second order type theory, ESOP'88, LNCS 300, pp 145\u2013159.","DOI":"10.1007\/3-540-19027-9_10"},{"key":"19_CR10","unstructured":"M. PARIGOT, Recursive programming with proofs, preprint 1988."}],"container-title":["Lecture Notes in Computer Science","CSL '89"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52753-2_47.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:25:12Z","timestamp":1605648312000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52753-2_47"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540527534","9783540471370"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-52753-2_47","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}