# Turing: a library to teach Introduction to the Theory of Computation (Fall'21)

**URL:** <https://discourse.rocq-prover.org/t/turing-a-library-to-teach-introduction-to-the-theory-of-computation-fall21/1478>\
**Category:** Announcements\
**Created:** [November 1, 2021, 12:23am UTC](https://discourse.rocq-prover.org/t/turing-a-library-to-teach-introduction-to-the-theory-of-computation-fall21/1478 "2021-11-01T00:23:57Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![AssertionError](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/assertionerror/32/604_2.png) [@AssertionError](https://discourse.rocq-prover.org/u/AssertionError)\
**Post date:** [November 1, 2021, 12:23am UTC](https://discourse.rocq-prover.org/t/turing-a-library-to-teach-introduction-to-the-theory-of-computation-fall21/1478/1 "2021-11-01T00:23:57Z")

</div>

The Turing project aims to offer the foundations of a course on introduction to the theory of computing. We are formalizing some content of the textbook Introduction to the Theory of Computation, by Michael Sipser.

> **[umb-svl / turing](https://gitlab.com/umb-svl/turing)**
>
> GitLab.com

Our library 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 library has been used to teach 3 sessions of a course on introduction to theory of computation at UMass Boston. Slides, video recordings, and classroom exercises are freely available here:

[https://cogumbreiro.github.io/teaching/cs420/f19/](https://cogumbreiro.github.io/teaching/cs420/f19/)  
[https://cogumbreiro.github.io/teaching/cs420/s20/](https://cogumbreiro.github.io/teaching/cs420/s20/)  
[https://cogumbreiro.github.io/teaching/cs420/f21/](https://cogumbreiro.github.io/teaching/cs420/f21/)

Some of the live coding recordings of S20 are available on YouTube: [Tiago Cogumbreiro - YouTube](https://www.youtube.com/channel/UCNm41xFudgHcUGGll_lSa5A/playlists?view=50&sort=dd&shelf_id=2)

I would love to meet other educators using a similar approach to teach intro to the theory of computation, and to connect with people curious to try out this work.

---

<div class="post-metadata">

**Author:** ![yforster](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/yforster/32/30_2.png) [@yforster](https://discourse.rocq-prover.org/u/yforster)\
**Post date:** [November 1, 2021, 4:05pm UTC](https://discourse.rocq-prover.org/t/turing-a-library-to-teach-introduction-to-the-theory-of-computation-fall21/1478/2 "2021-11-01T16:05:42Z")

</div>

That’s very interesting! I will try to have a closer look next week.

Until then: Are you aware of the following project?

> **[GitHub - uds-psl/coq-library-undecidability: A library of mechanised...](https://github.com/uds-psl/coq-library-undecidability/)**
>
> A library of mechanised undecidability proofs in the Coq proof assistant. - GitHub - uds-psl/coq-library-undecidability: A library of mechanised undecidability proofs in the Coq proof assistant.

---

<div class="post-metadata">

**Author:** ![AssertionError](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/assertionerror/32/604_2.png) [@AssertionError](https://discourse.rocq-prover.org/u/AssertionError)\
**Post date:** [November 1, 2021, 5:26pm UTC](https://discourse.rocq-prover.org/t/turing-a-library-to-teach-introduction-to-the-theory-of-computation-fall21/1478/3 "2021-11-01T17:26:35Z")

</div>

What a great resource! Thanks for the link.