During his summers at UofSC, Math and Computer Science Master's student Michael Levet taught CSE 355 Foundations of Computation, which serves as the terminal course in theoretical computer science for CS majors. The textbook for this course focused heavily on the procedures related to Automata Theory, often omitting the mathematical ideas or motivations for the procedures. Levet developed an extensive set of lecture notes for this course, with the express purpose of developing the theory in order to help students recognize and connect the key ideas. He also sought to help students draw connections between theoretical computer science and pure mathematics.

One of the high points is the discussion of the Brzozowski derivative, which allows one to recover a regular expression from a finite state machine by solving a system of linear recurrences over a semi-ring using the substitution method. While students are intimately familiar with solving systems of equations, this approach highlights ideas from combinatorics, algebra, and analysis. Some of these ideas include that regular expressions enumerate walks on the graph diagrams (i.e., regular expressions are walk-generating functions), an analogue between solving first-order recurrences over the integers compared to a semi-ring, and the fact that our system of linear recurrences correspond to the Jacobian matrix of the finite state machine.

As a result of Levet’s teaching, many of his students pursue opportunities to further explore theoretical computer science and mathematics, including minoring or double majoring in Math, as well as applying to graduate school in these areas. 

Levet's lecture notes now serve as recommended readings at other institutions, including at Stonybrook (CSE 303)  and the University of Otago in New Zealand (COSC 341).

An updated version of Levet's lecture notes can be found on his homepage.