A Mechanized Theory of Regular Trees in Dependent Type Theory

DOI10.1007/978-3-319-22102-1_27zbMath1465.68062OpenAlexW2396664939MaRDI QIDQ2945653

Régis Spadotti

Publication date: 14 September 2015

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://tel.archives-ouvertes.fr/tel-01589656/file/2016TOU30178b.pdf

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Data structures (68P05) Formalization of mathematics in connection with theorem provers (68V20) Type theory (03B38)

Related Items (1)

Finiteness and rational sequences, constructively

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Results on the propositional \(\mu\)-calculus
• Fundamental properties of infinite trees
• Macro tree transducers
• Generalized sequential machine maps
• Containers: Constructing strictly positive types
• Copatterns
• Subtyping, Declaratively
• Communicating sequential processes
• CoCaml: Functional Programming with Regular Coinductive Types
• Circular Coinduction in Coq Using Bisimulation-Up-To Techniques

This page was built for publication: A Mechanized Theory of Regular Trees in Dependent Type Theory