ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti

DOI10.1007/978-3-319-46750-4_26MaRDI QIDQ3179416zbMATHOpenAlexFDO

Authors 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)

Recommendations

• Termination Proofs for Recursive Functions in FoCaLiZe
• FoCaLiZe and Dedukti to the rescue for proof interoperability
• Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
• Typed Lambda Calculi and Applications
• Synthesis of ML programs in the system Coq

Cites work

• Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo
• Functional and Logic Programming
• Lambda calculus with patterns
• Objects and subtyping in the \(\lambda\)-\(\Pi\)-calculus modulo
• 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

Cited in

(3)

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

Describes a project that uses

Uses Software

• Coq
• Zenon
• FoCaLiZe

This page was built for publication: ML pattern-matching, recursion, and rewriting: from FoCaLiZe to Dedukti

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3179416)