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.
Type de document :
Communication dans un congrès
13th ICTAC International Colloquium on Theoretical Aspects of Computing, Oct 2016, Taipei, Taiwan. 13th ICTAC International Colloquium on Theoretical Aspects of Computing, pp.459 - 468, 2016, 〈http://cc.ee.ntu.edu.tw/~ictac2016/〉. 〈10.1007/978-3-319-46750-4_26〉
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01420638
Contributeur : Raphaël Cauderlier <>
Soumis le : mardi 20 décembre 2016 - 18:18:38
Dernière modification le : mardi 9 janvier 2018 - 14:13:30

Fichier

ICTAC_2016.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Raphaël Cauderlier, Catherine Dubois. ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti. 13th ICTAC International Colloquium on Theoretical Aspects of Computing, Oct 2016, Taipei, Taiwan. 13th ICTAC International Colloquium on Theoretical Aspects of Computing, pp.459 - 468, 2016, 〈http://cc.ee.ntu.edu.tw/~ictac2016/〉. 〈10.1007/978-3-319-46750-4_26〉. 〈hal-01420638〉

Partager

Métriques

Consultations de la notice

87

Téléchargements de fichiers

35