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

DOI10.1007/978-3-319-46750-4_26zbMATH Open1482.68267OpenAlexW2522260571MaRDI QIDQ3179416FDOQ3179416

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

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

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)

Cites Work

• 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
• Lambda calculus with patterns
• Functional and Logic Programming
• Objects and subtyping in the \(\lambda\)-\(\Pi\)-calculus modulo
• Termination Proofs for Recursive Functions in FoCaLiZe

Cited In (3)

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

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)