{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:11:53Z","timestamp":1725664313542},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540601173"},{"type":"electronic","value":"9783540494454"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60117-1_19","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:44:23Z","timestamp":1330278263000},"page":"335-350","source":"Crossref","is-referenced-by-count":0,"title":["Extracting programs with exceptions in an impredicative type system"],"prefix":"10.1007","author":[{"given":"Jean-Fran\u00e7ois","family":"Monin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"19_CR1","unstructured":"J-R. Abrial. The B-Book. Prentice Hall, 1994 (in preparation)."},{"key":"19_CR2","volume-title":"Handbook of Logic in Computer Science, vol 2","author":"H.P. Barendregt","year":"1992","unstructured":"H.P. Barendregt. Lambda Calculi with Types. In S. Abramsky & al., editors, Handbook of Logic in Computer Science, vol 2, S. Abramsky & al. Eds. Clarendon Press, Oxford, 1992."},{"key":"19_CR3","unstructured":"P. Cast\u00e9ran. Pro[gramm,v]ing with continuations: A development in Coq. Coq contribution, 1993 (available by FTP on ftp.inria.fr)."},{"key":"19_CR4","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Th. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Th. Coquand and C. Paulin-Mohring. Inductively defined types. In P. Martin-L\u00f6f and G. Mints, editors, Proceedings of Colog'88. Springer Verlag, 1990. LNCS 417.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"19_CR6","unstructured":"E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"19_CR7","unstructured":"G. Dowek & al. The Coq Proof Assistant User's Guide. version 5.8, INRIA-Rocquencourt et CNRS-ENS Lyon, f\u00e9v. 1993."},{"key":"19_CR8","first-page":"225","volume":"1","author":"J-Y. Girard","year":"1991","unstructured":"J-Y. Girard. A new constructive logic: classical logic. Mathematical Structures in Computer Science, vol 1, pp. 225\u2013296, 1991.","journal-title":"Mathematical Structures in Computer Science"},{"key":"19_CR9","unstructured":"J-Y. Girard, Y. Lafont, P. Taylor. Proofs and Types. Cambridge Univ. Press, vol 7, 1990."},{"key":"19_CR10","volume-title":"A formulae-as-types notion of control","author":"T. Griffin","year":"1990","unstructured":"T. Griffin. A formulae-as-types notion of control. POPL, Orlando, 1990."},{"key":"19_CR11","unstructured":"S. Hayashi, H. Nakano. PX, a Computational Logic. Foudations of Computing, MIT Press, 1988."},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"J.L. Lawall and O. Danvy. Separating Stages in Continuation-Passing Style Transformation. POPL, 1993.","DOI":"10.1145\/158511.158613"},{"key":"19_CR13","unstructured":"C. Morgan. Programming form Specification. Prentice Hall International Series in Computer Science. Prentice Hall, 1990."},{"key":"19_CR14","volume-title":"An evaluation semantics for classical proofs","author":"C. Murthy","year":"1991","unstructured":"C. Murthy. An evaluation semantics for classical proofs. LICS, Amsterdam, 1991."},{"key":"19_CR15","unstructured":"C. Paulin-Mohring. Extraction de programmes dans le calcul des constructions. th\u00e8se de doctorat de l'universit\u00e9 Paris VII, 1989."},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Inductive Definitions in the system Coq; Rules and Properties. In M. Bezem and J.F. Groote, editors, Proceedings of TLCA'93. Springer Verlag, 1993. LNCS 664.","DOI":"10.1007\/BFb0037116"},{"key":"19_CR17","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1016\/S0747-7171(06)80007-6","volume":"15","author":"C. Paulin-Mohring","year":"1993","unstructured":"C. Paulin-Mohring and B. Werner. Synthesis of ML Programs in the system Coq. Journal of Symbolic Computation, 15:607\u2013640, 1993.","journal-title":"Journal of Symbolic Computation"},{"key":"19_CR18","unstructured":"J. Rouyer. D\u00e9veloppement de l'algorithme d'unification dans le calcul des constructions avec types inductifs. Research Report 1795, INRIA-Lorraine, nov. 1992."}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60117-1_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:31:56Z","timestamp":1619573516000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60117-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540601173","9783540494454"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-60117-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}