{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:57:01Z","timestamp":1725533821134},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026133"},{"type":"electronic","value":"9783642026140"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02614-0_32","type":"book-chapter","created":{"date-parts":[[2009,7,2]],"date-time":"2009-07-02T07:47:24Z","timestamp":1246520844000},"page":"405-421","source":"Crossref","is-referenced-by-count":0,"title":["A Logically Saturated Extension of ${{\\bar\\lambda\\mu\\tilde{\\mu}}}$"],"prefix":"10.1007","author":[{"given":"Lionel Elie","family":"Mamane","sequence":"first","affiliation":[]},{"given":"Herman","family":"Geuvers","sequence":"additional","affiliation":[]},{"given":"James","family":"McKinna","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"32_CR1","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/11618027_16","volume-title":"Mathematical Knowledge Management","author":"C. Sacerdoti Coen","year":"2006","unstructured":"Sacerdoti Coen, C.: Explanation in natural language of lbmmt terms. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol.\u00a03863, pp. 234\u2013249. Springer, Heidelberg (2006)"},{"key":"32_CR2","unstructured":"Sacerdoti Coen, C.: Declarative representation of proof terms. In: Prog. Lang. for Mechanized Math., University of Linz. RISC Reports, vol.\u00a007-10, pp. 3\u201318 (2007)"},{"key":"32_CR3","unstructured":"Kirchner, F.: Interoperable proof systems. Ph.D thesis, \u00c9cole Polytechnique (2007)"},{"key":"32_CR4","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/11812289_7","volume-title":"Mathematical Knowledge Management","author":"S. Autexier","year":"2006","unstructured":"Autexier, S., Sacerdoti Coen, C.: A formal correspondence between OMDoc with alternative proofs and the \n                    \n                      \n                    \n                    ${{\\bar\\lambda\\mu\\tilde{\\mu}}}$\n                  -calculus. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.\u00a04108, pp. 67\u201381. Springer, Heidelberg (2006)"},{"key":"32_CR5","first-page":"233","volume-title":"ICFP 2000","author":"P.L. Curien","year":"2000","unstructured":"Curien, P.L., Herbelin, H.: The duality of computation. In: ICFP 2000, vol.\u00a035(9), pp. 233\u2013243. ACM, New York (2000)"},{"key":"32_CR6","unstructured":"Herbelin, H.: C\u2019est maintenant qu\u2019on calcule; au c\u0153ur de la dualit\u00e9. Habilitation \u00e0 diriger des recherches, Universit\u00e9 Paris 11 (December 2005)"},{"key":"32_CR7","unstructured":"Mamane, L.E., Geuvers, H., McKinna, J.: A logically saturated extension of \n                    \n                      \n                    \n                    ${{\\bar\\lambda\\mu\\tilde{\\mu}}}$\n                   to propositional logic, \n                    \n                      http:\/\/www.mamane.lu\/science\/lbmmt_extension\/"},{"key":"32_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-68103-8_5","volume-title":"Types for Proofs and Programs","author":"P. Corbineau","year":"2008","unstructured":"Corbineau, P.: A declarative proof language for the Coq proof assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol.\u00a04941, pp. 69\u201384. Springer, Heidelberg (2008)"},{"key":"32_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar - a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, p. 167. Springer, Heidelberg (1999)"},{"key":"32_CR10","series-title":"LNAI","first-page":"748","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"32_CR11","unstructured":"Trybulec, A.: Mizar language, \n                    \n                      http:\/\/mizar.org\/language\/"},{"issue":"1","key":"32_CR12","first-page":"27","volume":"38","author":"A. Asperti","year":"2003","unstructured":"Asperti, A., Guidi, F., Padovani, L., Sacerdoti Coen, C., Schena, I.: Mathematical knowledge management in HELM. AMAI\u00a038(1), 27\u201346 (2003)","journal-title":"AMAI"},{"key":"32_CR13","unstructured":"Coscoy, Y.: Explication textuelles de preuves pour le calcul des constructions inductives. Ph.D thesis, Universit\u00e9 de Nice-Sophia-Antipolis (September 2000)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02614-0_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,8]],"date-time":"2019-03-08T20:20:31Z","timestamp":1552076431000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02614-0_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026133","9783642026140"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02614-0_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}