{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:58:21Z","timestamp":1725551901052},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540314301"},{"type":"electronic","value":"9783540314318"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11618027_16","type":"book-chapter","created":{"date-parts":[[2006,1,19]],"date-time":"2006-01-19T11:48:07Z","timestamp":1137671287000},"page":"234-249","source":"Crossref","is-referenced-by-count":4,"title":["Explanation in Natural Language of \u03bb\u0304\u03bc\u03bc\u0342-Terms"],"prefix":"10.1007","author":[{"given":"Claudio Sacerdoti","family":"Coen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"16_CR1","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1023\/A:1022907629104","volume":"38","author":"A. Asperti","year":"2003","unstructured":"Asperti, A., Guidi, F., Padovani, L., Sacerdoti Coen, C., Schena, I.: Mathematical Knowledge Management in HELM. Annals of Mathematics and Artificial Intelligence\u00a038(1), 27\u201346 (2003)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"16_CR2","unstructured":"Asperti, A., Sacerdoti Coen, C.: Stylesheets to intermediate representation (prototypes D2.c-D2.d) and I. Loeb, Presentation stylesheets (prototypes D2.e-D2.f), technical reports of MoWGLI (project IST-2001-33562)"},{"key":"16_CR3","unstructured":"Coscoy, Y.: Explication textuelles de preuves pour le calcul des constructions inductives. PhD. thesis, Universit\u00e9 de Nice-Sophia-Antipolis (2000)"},{"issue":"1-2","key":"16_CR4","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/S0304-3975(99)00124-3","volume":"254","author":"T. Crolard","year":"2001","unstructured":"Crolard, T.: Subtractive logic. Theoretical computer science\u00a0254(1-2), 151\u2013185 (2001)","journal-title":"Theoretical computer science"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Curien, P., Herbelin, H.: The duality of computation. In: Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP 2000). SIGPLAN Notices, vol.\u00a035(9), pp. 233\u2013243. ACM, New York (2000), ISBN:1-58113-2-2-6","DOI":"10.1145\/351240.351262"},{"key":"16_CR6","unstructured":"Herbelin, H.: S\u00e9quents qu\u2019on calcule: de l\u2019interpr\u00e9tation du calcul des s\u00e9quents comme calcul de lambda-terms et comme calcul de strat\u00e9gies gagnantes. PhD. thesis (1995)"},{"key":"16_CR7","unstructured":"Kohlhase, M.: OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2)"},{"key":"16_CR8","volume-title":"Electronic Notes in Theoretical Computer Science","author":"S. Lengrand","year":"2003","unstructured":"Lengrand, S.: Call-by-value, call-by-name, and strong normalization for the classical sequent calculus. In: Gramlich, B., Lucas, S. (eds.) Electronic Notes in Theoretical Computer Science, vol.\u00a086(4). Elsevier, Amsterdam (2003)"},{"key":"16_CR9","unstructured":"Parigot, M.: \u03bb\u03bc-calculus: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol.\u00a0624. Springer, Heidelberg (1992)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-24849-1_24","volume-title":"Types for Proofs and Programs","author":"F. Wiedijk","year":"2004","unstructured":"Wiedijk, F.: Formal Proof Sketches. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 378\u2013393. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11618027_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:12:04Z","timestamp":1619507524000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11618027_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540314301","9783540314318"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/11618027_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}