ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti

DOI10.1007/978-3-319-46750-4_26zbMath1482.68267MaRDI QIDQ3179416

Catherine Dubois, Raphaël Cauderlier

Publication date: 21 December 2016

Published in: Theoretical Aspects of Computing – ICTAC 2016 (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01420638/file/ICTAC_2016.pdf

Mathematics Subject Classification ID

68N15: Theory of programming languages

68N20: Theory of compilers and interpreters

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Related Items

dedukti

Uses Software

• Coq
• Zenon
• FoCaLiZe