Skip to Main content Skip to Navigation
Master thesis

Representing Agda and coinduction in the λΠ-calculus modulo rewriting

Thiago Felicissimo 1 
1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
Inria Saclay - Ile de France, LMF - Laboratoire Méthodes Formelles
Abstract : 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.
Complete list of metadata
Contributor : Thiago Felicissimo Connect in order to contact the contributor
Submitted on : Tuesday, September 14, 2021 - 12:51:25 PM
Last modification on : Friday, August 5, 2022 - 2:58:08 PM
Long-term archiving on: : Wednesday, December 15, 2021 - 6:30:40 PM


Files produced by the author(s)


  • HAL Id : hal-03343699, version 1


Thiago Felicissimo. Representing Agda and coinduction in the λΠ-calculus modulo rewriting. Logic in Computer Science [cs.LO]. 2021. ⟨hal-03343699⟩



Record views


Files downloads