Skip to Main content Skip to Navigation

A mechanized theory of regular trees in dependent type theory

Abstract : We propose two characterizations of regular trees. The first one is semantic and is based on coinductive types. The second one is syntactic and represents regular trees by means of cyclic terms. We prove that both of these characterizations are isomorphic. Then, we study the problem of defining tree morphisms preserving the regularity property. We show, by using the formalism of tree transducers, the existence of syntactic criterion ensuring that this property is preserved. Finally, we consider applications of the theory of regular trees such as the definition of the parallel composition operator of a process algebra or, the decidability problems on regular trees through a mechanization of a model-checker for a coalgebraic mu-calculus. All the results were mechanized and proved correct in the Coq proof assistant.
Document type :
Complete list of metadata

Cited literature [78 references]  Display  Hide  Download
Contributor : Abes Star :  Contact
Submitted on : Monday, September 18, 2017 - 6:34:16 PM
Last modification on : Wednesday, March 17, 2021 - 9:46:04 AM


Version validated by the jury (STAR)


  • HAL Id : tel-01589656, version 1



Régis Spadotti. A mechanized theory of regular trees in dependent type theory. Mathematical Software [cs.MS]. Université Paul Sabatier - Toulouse III, 2016. English. ⟨NNT : 2016TOU30178⟩. ⟨tel-01589656⟩



Record views


Files downloads