Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Regular language representations in the constructive type theory of Coq
Doczkal C., Smolka G. Journal of Automated Reasoning61 (1-4):521-553,2018.Type:Article
Date Reviewed: Aug 16 2018

Theoretical computer science is traditionally presented using paper and pencil, with little emphasis on formal correctness and completeness in detail. This provides a backdoor for ambiguities, gaps, and errors. However, nowadays, powerful semi-interactive proving systems such as Isabelle and Coq are able to put theoretical work on a much firmer basis.

This is demonstrated in the paper’s use of Coq for formalizing the theory of regular language representations, that is, various forms of automata, regular expressions, and the weak monadic second-order logic (WMSO) theory of one successor relation (WS1S). On the surface, the presentation resembles a recapitulation of known results in a classical style. What makes it special is that each definition, theorem, and proof is actually the outline of a counterpart in Coq; the paper is thus a companion to the formal Coq theory of regular languages that is available online, where all proofs have been mechanically constructed and respectively checked.

The paper demonstrates how the constructive type theory of Coq can be used in an elegant way to develop the essential notions. In particular, it shows how the original proofs have to be rethought in terms of constructive type theory, which also yields novel insights such as a new constructive version of the Myhill-Nerode theorem. This interesting paper documents the experience gained from developing 3000 lines of Coq code. It will hopefully inspire researchers to integrate proof assistants into their own work.

Reviewer:  Wolfgang Schreiner Review #: CR146206 (1810-0540)
Bookmark and Share
  Featured Reviewer  
 
Automata (F.1.1 ... )
 
 
Proof Theory (F.4.1 ... )
 
 
Deduction And Theorem Proving (I.2.3 )
 
 
Mathematical Software (G.4 )
 
Would you recommend this review?
yes
no
Other reviews under "Automata": Date
The congruence theory of closure properties of regular tree languages
Tirri S. Theoretical Computer Science 76(2-3): 261-271, 2001. Type: Article
Jun 1 1991
Distribution and synchronized automata
Petit A. Theoretical Computer Science 76(2-3): 285-308, 2001. Type: Article
Feb 1 1992
Efficient simulation of finite automata by neural nets
Alon N., Dewdney A., Ott T. Journal of the ACM 38(2): 495-514, 1991. Type: Article
Dec 1 1991
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy