{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:20Z","timestamp":1761611300588},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540605799"},{"type":"electronic","value":"9783540477709"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60579-7_5","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T20:42:56Z","timestamp":1330288976000},"page":"83-100","source":"Crossref","is-referenced-by-count":4,"title":["A user's friendly syntax to define recursive functions as typed \u03bb-terms"],"prefix":"10.1007","author":[{"given":"Pascal","family":"Manoury","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"5_CR1","unstructured":"H. Barendregt The Lambda Calculus, its Syntax and Semantics; North Holland, 1981, 1984."},{"key":"5_CR2","unstructured":"C. Cornes et al. The Coq Proof Assistant Reference Manual Version 5.10; Internal Report INRIA."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"K. G\u00f6del \u00dcber eine bisher noch nicht Erweiterung des finiten Standpunktes; Dialectica 12, 1958.","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"W. Hodge, B. Watson On a hitherto unexploited extension of finitary standpoint; J.P.L. 9, 1980, english translation of [3].","DOI":"10.1007\/BF00247744"},{"key":"5_CR5","unstructured":"W.A. Howard The formul\u00e6-as-types notion of construction; in J.R. Hindley, editor, To H.B. Curry: Essays on Combinatory Logic, lambda-calculus and formalism, Seidin, J.P. 1980."},{"key":"5_CR6","unstructured":"J.L Krivine, M. Parigot Programming with proofs; in SCT 87 (1987), Wendish-Rietz; in EIK 26 (1990) pp 146\u2013167."},{"key":"5_CR7","unstructured":"P. Martin-L\u00f6f Intuitionistic Type Theory; Studies in Proof Theory. Bibliopolis, 1984."},{"key":"5_CR8","unstructured":"P. Manoury, M. Parigot, M. Simonot ProPre: a programming language with proofs; in proceedings LPAR 92, LNAI 624."},{"key":"5_CR9","unstructured":"P. Manoury and M. Simonot Des preuves de totalit\u00e9 de fonctions comme synth\u00e8se de programmes; Phd Thesis, Universit\u00e9 Paris 7, December 1992."},{"key":"5_CR10","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/0304-3975(94)00021-2","volume":"135","author":"P. Manoury","year":"1994","unstructured":"P. Manoury and M. Simonot Automatizing termination proof of recurslvely defined functions; in TCS, 135 (1994), pp 319\u2013343.","journal-title":"TCS"},{"key":"5_CR11","volume-title":"PhD thesis","author":"C. Parent","year":"1995","unstructured":"C. Parent Synthese de preuves de programmes dans le Calcul des Constrctions Inductives; PhD thesis, ENS Lyon, January 1995."},{"key":"5_CR12","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1016\/0304-3975(92)90042-E","volume":"94","author":"M. Parigot","year":"1992","unstructured":"M. Parigot Recursive programming with proofs; in TCS 94 (1992) pp 335\u2013356.","journal-title":"TCS"},{"key":"5_CR13","unstructured":"C. Paulin-Mohring Inductive Definitions in the System Cog \u2014 Rules and properties; proceedings TLCA 93, LNCS 664 (1993)."},{"key":"5_CR14","unstructured":"B. Werner Une th\u00e9orie des constructions inductives; Phd Thesis, Universit\u00e9 Paris 7, May 1994."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60579-7_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:59:54Z","timestamp":1605646794000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60579-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540605799","9783540477709"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-60579-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}