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

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

Raphaël Cauderlier, Catherine Dubois

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

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

FoCaLiZe and Dedukti to the rescue for proof interoperability, First-order automated reasoning with theories: when deduction modulo theory meets practice, dedukti

Uses Software

• Coq
• Zenon
• FoCaLiZe

Cites Work

• Unnamed Item
• Lambda calculus with patterns
• Termination Proofs for Recursive Functions in FoCaLiZe
• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• Functional and Logic Programming