{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:11:50Z","timestamp":1725664310641},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540601173"},{"type":"electronic","value":"9783540494454"}],"license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60117-1_20","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:44:21Z","timestamp":1330278261000},"page":"351-379","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Synthesizing proofs from programs in the Calculus of Inductive Constructions"],"prefix":"10.1007","author":[{"given":"Catherine","family":"Parent","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"20_CR1","unstructured":"H. Barendregt. Lambda Calculi with Types. Technical Report 91-19, Catholic University Nijmegen, September 1991."},{"key":"20_CR2","unstructured":"R. Burstall and J. McKinna. Deliverables: a categorical approach to program development in type theory. Technical Report 92-242, LFCS, October 1992. Also in [NPP92]."},{"key":"20_CR3","unstructured":"C. Cornes, J. Courant, J.C. Filli\u00e2tre, G. Huet, P. Manoury, C. Paulin-Mohring, C. Mu\u00f1oz, C. Murthy, C. Parent, A. Sa\u00efbi, and B. Werner. Coq V5.10 Reference Manual. Technical report, 1994. Disponible en ftp anonyme sur ftp.inria.fr, \u00e0 para\u00eetre."},{"key":"20_CR4","unstructured":"R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986."},{"key":"20_CR5","unstructured":"T. Coquand. Une th\u00e9orie des constructions. PhD thesis, Universit\u00e9 Paris VII, 1985."},{"key":"20_CR6","unstructured":"G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq Proof Assistant User's Guide \u2014 Version 5.8. Technical Report 154, Projet Formel \u2014 INRIA-Rocquencourt-CNRS-ENS Lyon, May 1993."},{"key":"20_CR7","unstructured":"J.Y. Girard. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris 7, 1972."},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM, 12(10), October 1969.","DOI":"10.1145\/363235.363259"},{"key":"20_CR9","unstructured":"W.A. Howard. The formulaes-as-types notion of construction. In J.R. Hindley, editor, To H.B.Curry: Essays on Combinatory Logic, lambda-calculus and formalism. Seldin, J.P., 1980."},{"key":"20_CR10","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory. Studies in Proof Theory. Bibliopolis, 1984."},{"key":"20_CR11","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":"20_CR12","unstructured":"B. Nordstr\u00f6m, K. Petersson, and G. Plotkin, editors. Proceedings of the 1992 workshop on types for proofs and programs, June 1992."},{"key":"20_CR13","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J. M. Smith. Programming in Martin-L\u00f6f 's Type Theory: an introduction. Oxford Science Publications, 1990."},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"C. Parent. Developing certified programs in the system Coq \u2014 The Program tactic. In H. Barendregt and T. Nipkow, editors, Types For Proofs and Programs, volume 806 of LNCS, pages 291\u2013312, May 1993.","DOI":"10.1007\/3-540-58085-9_81"},{"key":"20_CR15","unstructured":"C. Parent. Synth\u00e8se de preuves de programmes dans le Calcul des Constructions. PhD thesis, Ecole Normale Sup\u00e9rieure de Lyon, January 1995."},{"key":"20_CR16","first-page":"209","volume":"442","author":"F. Pfenning","year":"1989","unstructured":"F. Pfenning and Paulin-Mohring C. Inductively Defined Types in the Calculus of Constructions. In 5th International Conference on Mathematical Foundations of Programming Semantics, volume 442 of LNCS, pages 209\u2013228, 1989.","journal-title":"LNCS"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Extracting F\n\u03c9 programs from proofs in the Calculus of Constructions. In Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, January 1989.","DOI":"10.1145\/75277.75285"},{"key":"20_CR18","unstructured":"C. Paulin-Mohring. Extraction de programmes dans le Calcul des Constructions. PhD thesis, Universit\u00e9 Paris VII, 1989."},{"key":"20_CR19","unstructured":"C. Paulin-Mohring. Inductive Definitions in the System Coq \u2014 Rules and Properties. In Typed Lambda Calculi and Applications, volume 664 of LNCS, March 1993. Also in research report 92-49, LIP-ENS Lyon, December 1992."},{"key":"20_CR20","unstructured":"E. Poll. A Programming Logic Based on Type Theory. PhD thesis, Technische Universiteit Eindhoven, 1994."}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60117-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:33:11Z","timestamp":1558269191000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60117-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540601173","9783540494454"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-60117-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]},"assertion":[{"value":"3 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}