A mechanized theory of regular trees in dependent type theory
DOI10.1007/978-3-319-22102-1_27zbMATH Open1465.68062OpenAlexW2396664939MaRDI QIDQ2945653FDOQ2945653
Authors: 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
Recommendations
Formal languages and automata (68Q45) Data structures (68P05) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Type theory (03B38)
Cites Work
- CoCaml: functional programming with regular coinductive types
- Containers: Constructing strictly positive types
- Communicating sequential processes
- Results on the propositional \(\mu\)-calculus
- Fundamental properties of infinite trees
- Title not available (Why is that?)
- Generalized sequential machine maps
- Title not available (Why is that?)
- Macro tree transducers
- Title not available (Why is that?)
- Subtyping, declaratively. An exercise in mixed induction and coinduction
- Circular coinduction in Coq using bisimulation-up-to techniques
- Copatterns, programming infinite structures by observations
- Title not available (Why is that?)
Cited In (4)
Uses Software
This page was built for publication: A mechanized theory of regular trees in dependent type theory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945653)