The Turing project aims to offer the foundations of the Theory of Computation formalized in Coq. This includes results on

• Formal languages: common operators and language equality results
• Regular languages: regular expressions, pumping lemma
• Turing machines: acceptance, equality, map-reducibility, decidability.

This project is led by Tiago Cogumbreiro to support teaching an undergraduate course on Theory of Computing, CS 420, at UMass Boston. See Tiago's archives of Fall'20 to access the teaching material.

• Step 1. Install scoop
• Step 2. Open powershell and run:

> scoop install https://gitlab.com/cogumbreiro/turing/-/raw/master/scoop/turing.json

To install the Turing library in your system run these commands:

$ git clone https://gitlab.com/cogumbreiro/turing
$ cd turing
$ ./configure.sh
$ make
$ make install

Make sure you have already installed Turing in your system.

• Step 1. Open a powershell prompt and run

> scoop update turing

Then, run the following commands:

$ cd /path/where/you/installed/turing
$ git pull
$ make
$ make install

In this project, we are formalizing some content of the textbook Introduction to the Theory of Computation, by Michael Sipser, 3^rd edition.

• Theorem 1.70: Pumping lemma for regular languages
• Example 1.73: $\{ 0^n 1^n \mid n \ge 0 \}$ is not regular

• Theorem 4.11: $A_{\mathsf{TM}}$ is undecidable.
• Corollary 4.18: Some languages are not recognizable.
• Theorem 4.22: $L$ is decidable iff $L$ is recognizable and co-recognizable
• Theorem 4.23: $\overline{A}_{\mathsf{TM}}$ is not recognizable.

• Theorem 5.1: $HALT_{\mathsf{TM}}$ is undecidable.
• Theorem 5.2: $E_{\mathsf{TM}}$ is undecidable.
• Theorem 5.4: $EQ_{\mathsf{TM}}$ is undedicable.
• Theorem 5.22: If $A \le_{\mathrm{m}} B$ and $A$ decidable, then $B$ decidable.
• Theorem 5.28: If $A \le_{\mathrm{m}} B$ and $A$ recognizable, then $B$ recognizable.
• Corollary 5.29: If $A \le_{\mathrm{m}} B$ and $B$ is undecidable, then $A$ is undecidable.
• Corollary 5.30: $EQ_{\mathsf{TM}}$ unrecognizable and co-unrecognizable.