Regular language representations in the constructive type theory of Coq
type: Item
instance of: scholarly article
title: Regular language representations in the constructive type theory of Coq
zbMATH Open document ID: 1451.68146
author: Christian Doczkal
author: Gert Smolka
published in: Journal of Automated Reasoning
publication date: 2018-08-21T00:00:00Z
Mathematics Subject Classification ID: 68Q45
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03D05
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 6921423
zbMATH Keywords: regular languages
zbMATH Keywords: two-way automata
zbMATH Keywords: WS1S
zbMATH Keywords: constructive type theory
zbMATH Keywords: interactive theorem proving
zbMATH Keywords: Coq
zbMATH Keywords: SSReflect
describes a project that uses: Coq
describes a project that uses: MSO_Regex_Equivalence
describes a project that uses: Coq/SSReflect
describes a project that uses: Myhill-Nerode
describes a project that uses: Presburger Automata
describes a project that uses: Regular Sets
describes a project that uses: Finite Automata HF
describes a project that uses: Hereditarily Finite Sets
describes a project that uses: GitHub
MaRDI profile type: Publication
full work available at URL: s10817-018-9460-x
OpenAlex ID: W2791390006
cites work: Explicit substitutions
cites work: Formalizing the Logic-Automaton Connection
cites work: Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings
cites work: Deciding Kleene algebras in \texttt{Coq}
cites work: Derivatives of Regular Expressions
cites work: Weak Second‐Order Arithmetic and Finite Automata
cites work: Pragmatic Quotient Types in Coq
cites work: A Decision Procedure for Regular Expression Equivalence in Type Theory
cites work: A Constructive Theory of Regular Languages in Coq
cites work: Two-Way Automata in Coq
cites work: Decision Problems of Finite Automata Design and Related Arithmetics
cites work: Q5747095
cites work: Succinctness of the Complement and Intersection of Regular Expressions
cites work: A Modular Formalisation of Finite Group Theory
cites work: Deciding Kleene algebra terms equivalence in Coq
cites work: A coherence theorem for Martin-Löf's type theory
cites work: Automatentheorie und Logik
cites work: Q4506483
cites work: Automata theory and its applications
cites work: Q4344149
cites work: Proof Pearl: regular expression equivalence and relation algebra
cites work: A Formalisation of Finite Automata Using Hereditarily Finite Sets
cites work: Kleene Algebra with Tests and Coq Tools for while Programs
cites work: Q5541339
cites work: The Complexity of Translating Logic to Finite Automata
cites work: Q5541340
cites work: Structural Analysis of Narratives with the Coq Proof Assistant
cites work: Verified decision procedures for MSO on words based on derivatives of regular expressions
cites work: A note on the reduction of two-way automata to one-way automata
cites work: Endmarkers can make a difference
cites work: A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
cites work: A formalisation of the Myhill-Nerode theorem based on regular expressions
Wikidata QID: Q130137861
DOI: 10.1007/S10817-018-9460-X
description: scientific article; zbMATH DE number 6921423