Skip to Main content Skip to Navigation
Conference papers

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

Abstract : The programming environment FoCaLiZe allows the user to specify, implement, and prove programs with the help of the theorem prover Zenon. In the actual version, those proofs are verified by Coq. In this paper we propose to extend the FoCaLiZe compiler by a backend to the Dedukti language in order to benefit from Zenon Modulo, an extension of Zenon for Deduction modulo. By doing so, FoCaLiZe can benefit from a technique for finding and verifying proofs more quickly. The paper focuses mainly on the process that overcomes the lack of local pattern-matching and recursive definitions in Dedukti.
Document type :
Conference papers
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-01420638
Contributor : Raphaël Cauderlier <>
Submitted on : Tuesday, December 20, 2016 - 6:18:38 PM
Last modification on : Tuesday, July 7, 2020 - 11:52:47 AM

File

ICTAC_2016.pdf
Files produced by the author(s)

Identifiers

Citation

Raphaël Cauderlier, Catherine Dubois. ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti. ICTAC 2016 - 13th International Colloquium on Theoretical Aspects of Computing, Oct 2016, Taipei, Taiwan. pp.459-468, ⟨10.1007/978-3-319-46750-4_26⟩. ⟨hal-01420638⟩

Share

Metrics

Record views

270

Files downloads

462