Representing Agda and coinduction in the λΠ-calculus modulo rewriting
Résumé
Coinduction is a principle, or a proof technique, dual to induction and which allows to handle possibly infinite objects in a natural way, such as infinite lists, infinite trees, formal languages, non well-founded sets, etc. Because of its usefulness, it is increasingly being added to proof assistants, such as Coq, Isabelle, PVS and Agda. In order to be able to translate proofs by coinduction coming from multiple proof assistants it is thus important to first understand how to encode coinduction in Dedukti, a problem that had never been addressed before. During this internship, we studied the representation of Agda and coinduction in Dedukti. Among the techniques of implementing coinduction in proof assistants, Agda features two presentations: musical coinduction and copattern coinduction. Based on their internal syntax representation in Agda, we proposed an encoding of both presentations in Dedukti. We resumed the development of the Agda2Dedukti translator and extended it with the proposed encoding, allowing it to translate automatically proofs by coinduction into Dedukti.
Origine : Fichiers produits par l'(les) auteur(s)