Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
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 metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Raphaël Cauderlier Connect in order to contact the contributor
Submitted on : Tuesday, December 20, 2016 - 6:18:38 PM
Last modification on : Monday, February 21, 2022 - 3:38:12 PM


Files produced by the author(s)



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⟩



Record views


Files downloads