{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T05:23:33Z","timestamp":1742966613170,"version":"3.40.3"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_24","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"371-388","source":"Crossref","is-referenced-by-count":3,"title":["Typing Total Recursive Functions in Coq"],"prefix":"10.1007","author":[{"given":"Dominique","family":"Larchey-Wendling","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)"},{"issue":"4","key":"24_CR2","doi-asserted-by":"publisher","first-page":"671","DOI":"10.1017\/S0960129505004822","volume":"15","author":"A Bove","year":"2005","unstructured":"Bove, A., Capretta, V.: Modelling general recursion in type theory. Math. Struct. Comput. Sci. 15(4), 671\u2013708 (2005)","journal-title":"Math. Struct. Comput. Sci."},{"key":"24_CR3","unstructured":"Cast\u00e9ran, P.: Utilisation en Coq de l\u2019op\u00e9rateur de description (2007). http:\/\/jfla.inria.fr\/2007\/actes\/PDF\/03_casteran.pdf"},{"key":"24_CR4","unstructured":"Coen, C.S., Valentini, S.: General recursion and formal topology. In: Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, EPiC Series, Edinburgh, UK, 15 July 2010, vol. 5, pp. 71\u201382. EasyChair (2010)"},{"key":"24_CR5","volume-title":"Proofs and Types","author":"JY Girard","year":"1989","unstructured":"Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, New York (1989)"},{"key":"24_CR6","series-title":"Ellis Horwood Series in Computers and Their Applications","volume-title":"Lambda-Calculus, Types and Models","author":"J Krivine","year":"1993","unstructured":"Krivine, J.: Lambda-Calculus, Types and Models. Ellis Horwood Series in Computers and Their Applications. Ellis Horwood, Masson (1993)"},{"key":"24_CR7","unstructured":"Larchey-Wendling, D.: A constructive mechanization of Lambda Calculus in Coq (2017). http:\/\/www.loria.fr\/~larchey\/Lambda_Calculus"},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-642-22863-6_22","volume-title":"Interactive Theorem Proving","author":"M Norrish","year":"2011","unstructured":"Norrish, M.: Mechanised computability theory. In: Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 297\u2013311. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-22863-6_22"},{"key":"24_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02460-7","volume-title":"Recursively Enumerable Sets and Degrees","author":"RI Soare","year":"1987","unstructured":"Soare, R.I.: Recursively Enumerable Sets and Degrees. Springer-Verlag New York Inc., New York (1987)"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/BFb0014566","volume-title":"Theoretical Aspects of Computer Software","author":"B Werner","year":"1997","unstructured":"Werner, B.: Sets in types, types in sets. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 530\u2013546. Springer, Heidelberg (1997). doi:10.1007\/BFb0014566"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-39634-2_13","volume-title":"Interactive Theorem Proving","author":"J Xu","year":"2013","unstructured":"Xu, J., Zhang, X., Urban, C.: Mechanising turing machines and computability theory in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 147\u2013162. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39634-2_13"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1007\/BFb0105420","volume-title":"Theorem Proving in Higher Order Logics","author":"V Zammit","year":"1996","unstructured":"Zammit, V.: A mechanisation of computability theory in HOL. In: Goos, G., Hartmanis, J., Leeuwen, J., Wright, J., Grundy, J., Harrison, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 431\u2013446. Springer, Heidelberg (1996). doi:10.1007\/BFb0105420"},{"key":"24_CR13","unstructured":"Zammit, V.: A proof of the S-m-n theorem in Coq. Technical report, The Computing Laboratory, The University of Kent, Canterbury, Kent, UK, March 1997. http:\/\/kar.kent.ac.uk\/21524\/"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T06:07:57Z","timestamp":1664431677000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}