{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T04:13:30Z","timestamp":1749615210050,"version":"3.41.0"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319467498"},{"type":"electronic","value":"9783319467504"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-46750-4_26","type":"book-chapter","created":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T02:11:57Z","timestamp":1474423917000},"page":"459-468","source":"Crossref","is-referenced-by-count":3,"title":["ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti"],"prefix":"10.1007","author":[{"given":"Rapha\u00ebl","family":"Cauderlier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Catherine","family":"Dubois","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"key":"26_CR1","unstructured":"Assaf, A.: A framework for defining computational higher-order logics. Ph.D. thesis, \u00c9cole Polytechnique (2015)"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Assaf, A., Burel, G.: Translating HOL to Dedukti. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings Fourth Workshop on Proof eXchange for Theorem Proving. EPTCS, vol. 186, Berlin, Germany, pp. 74\u201388 (2015)","DOI":"10.4204\/EPTCS.186.8"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-75560-9_13","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R Bonichon","year":"2007","unstructured":"Bonichon, R., Delahaye, D., Doligez, D.: Zenon: an extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 151\u2013165. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-75560-9_13"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Burel, G.: A shallow embedding of resolution and superposition proofs into the $$\\lambda {\\varPi }$$ -calculus modulo. In: Blanchette, J.C., Urban, J. (eds.) PxTP 2013. 3rd International Workshop on Proof Exchange for Theorem Proving. EasyChair Proceedings in Computing, vol. 14, Lake Placid, USA, pp. 43\u201357 (2013)","DOI":"10.29007\/ftc2"},{"key":"26_CR5","unstructured":"Cauderlier, R.: Object-oriented mechanisms for interoperability between proof systems. Ph.D. thesis, Conservatoire National des Arts et M\u00e9tiers, Paris (draft)"},{"key":"26_CR6","unstructured":"Cauderlier, R., Dubois, C.: Objects and subtyping in the $$\\lambda \\varPi $$ -calculus modulo. In: Post-proceedings of the 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl, Paris (2014)"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Cauderlier, R., Halmagrand, P.: Checking Zenon Modulo proofs in Dedukti. In: Kaliszyk, C., Paskevich, A. (eds.) Proceedings 4th Workshop on Proof eXchange for Theorem Proving. EPTCS, vol. 186, Berlin, Germany, pp. 57\u201373 (2015)","DOI":"10.4204\/EPTCS.186.7"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-73228-0_9","volume-title":"Typed Lambda Calculi and Applications","author":"D Cousineau","year":"2007","unstructured":"Cousineau, D., Dowek, G.: Embedding pure type systems in the $$\\lambda {\\varPi }$$ -calculus modulo. In: Rocca, S.R.D. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 102\u2013117. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-73228-0_9"},{"key":"26_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-642-45221-5_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Delahaye","year":"2013","unstructured":"Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Zenon Modulo: when Achilles outruns the tortoise using deduction modulo. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19. LNCS, vol. 8312, pp. 274\u2013290. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-45221-5_20"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-319-39110-6_8","volume-title":"Trends in Functional Programming","author":"C Dubois","year":"2016","unstructured":"Dubois, C., Pessaux, F.: Termination proofs for recursive functions in FoCaLiZe. In: Serrano, M., Hage, J. (eds.) TFP 2015. LNCS, vol. 9547, pp. 136\u2013156. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-39110-6_8"},{"issue":"2","key":"26_CR11","doi-asserted-by":"crossref","first-page":"7:1","DOI":"10.1145\/1890028.1890030","volume":"33","author":"J Giesl","year":"2011","unstructured":"Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for Haskell by term rewriting. ACM Trans. Program. Lang. Syst. 33(2), 7:1\u20137:39 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-540-24754-8_20","volume-title":"Functional and Logic Programming","author":"W Kahl","year":"2004","unstructured":"Kahl, W.: Basic pattern matching calculi: a fresh view on matching failure. In: Kameyama, Y., Stuckey, P.J. (eds.) FLOPS 2004. LNCS, vol. 2998, pp. 276\u2013290. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24754-8_20"},{"issue":"1\u20133","key":"26_CR13","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1016\/j.tcs.2008.01.019","volume":"398","author":"JW Klop","year":"2008","unstructured":"Klop, J.W., van Oostrom, V., de Vrijer, R.: Lambda calculus with patterns. Theoret. Comput. Sci. 398(1\u20133), 16\u201331 (2008). Calculi, Types and Applications: Essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi Della Rocca","journal-title":"Theoret. Comput. Sci."},{"key":"26_CR14","unstructured":"Lucas, S., Pe\u00f1a, R.: Rewriting techniques for analysing termination and complexity bounds of Safe programs. In: LOPSTR 2008, pp. 43\u201357 (2008)"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Pessaux, F.: FoCaLiZe: inside an F-IDE. In: Dubois, C., Giannakopoulou, D., M\u00e9ry, D. (eds.) Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014. EPTCS, vol. 149, Grenoble, France, pp. 64\u201378 (2014)","DOI":"10.4204\/EPTCS.149.7"},{"key":"26_CR16","series-title":"Prentice-Hall International Series in Computer Science","volume-title":"The Implementation of Functional Programming Languages","author":"SL Peyton Jones","year":"1987","unstructured":"Peyton Jones, S.L.: The Implementation of Functional Programming Languages. Prentice-Hall International Series in Computer Science. Prentice-Hall, Inc., Upper Saddle River (1987)"},{"key":"26_CR17","unstructured":"Saillard, R.: Type checking in the $$\\lambda {\\varPi }$$ -calculus modulo: theory and practice. Ph.D. thesis, MINES Paritech (2015)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2016"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46750-4_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T20:22:36Z","timestamp":1749586956000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46750-4_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319467498","9783319467504"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46750-4_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}