A mechanized theory of regular trees in dependent type theory

DOI10.1007/978-3-319-22102-1_27MaRDI QIDQ2945653zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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)

Recommendations

• Types for Proofs and Programs
• Regular language representations in the constructive type theory of Coq
• A constructive theory of regular languages in Coq
• scientific article; zbMATH DE number 2087543
• scientific article; zbMATH DE number 3911742

Cites work

• scientific article; zbMATH DE number 5757682 (Why is no real title available?)
• scientific article; zbMATH DE number 1183236 (Why is no real title available?)
• scientific article; zbMATH DE number 3566209 (Why is no real title available?)
• scientific article; zbMATH DE number 1424053 (Why is no real title available?)
• Circular coinduction in Coq using bisimulation-up-to techniques
• CoCaml: functional programming with regular coinductive types
• Communicating sequential processes
• Containers: Constructing strictly positive types
• Copatterns, programming infinite structures by observations
• Fundamental properties of infinite trees
• Generalized sequential machine maps
• Macro tree transducers
• Results on the propositional \(\mu\)-calculus
• Subtyping, declaratively. An exercise in mixed induction and coinduction

Cited in

(4)

• scientific article; zbMATH DE number 2087543 (Why is no real title available?)
• scientific article; zbMATH DE number 1863396 (Why is no real title available?)
• Types for Proofs and Programs
• Finiteness and rational sequences, constructively

Describes a project that uses

Uses Software

• Coq

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)