Skip to Main content Skip to Navigation
Theses

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 :
Theses
Complete list of metadata

Cited literature [78 references]  Display  Hide  Download

https://tel.archives-ouvertes.fr/tel-01589656
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

File

2016TOU30178b.pdf
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-01589656, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

254

Files downloads

410