Algorithms that are the main driver behind a system are, in my opinion, easier to find in non-algorithms courses for the same reason theorems with immediate applications are easier to find in applied ...

I have personally enjoyed several Aha! moments from studying basic automata theory. NFAs and DFAs form a microcosm for theoretical computer science as a whole. Does Non-determinism Lead to ...

Can you hear that noise? It is the sound of a thousand brilliant theorems, applications and tools laughing in automata-theoretic heaven. Languages and automata are elegant and robust concepts that ...

I used to like quirky titles when I started out in computer science but got bored eventually. Some authors manage to write titles that are clever, memorable and relevant but most attempts at funny ...

Topology is such a mature discipline with varied subfields including geometric, algebraic, metric, point-set and (the self deprecating) pointless topology. Computer science is also fairly broad and ...

The undecidability of the halting problem. Beautiful for many reasons. It is an impossibility result. The proof uses diagonalisation. The statement applies to a broad range of models of computation. ...

What you are doing is deriving a topological representation of a Boolean algebra. The study of representations of Boolean algebras goes back at least to Lindenbaum and Tarski who proved (in 1925, I ...

Your question itself is not naive but the type of answer you ask for is. It is rare for any line of work or intellectual enquiry to have an elevator pitch explanation. Not all would agree with your ...

The question is, in my opinion, quite vague and involves some misunderstanding, so this answer attempts only to provide the right vocabulary and point you in the right direction. There are two fields ...

The quick summary is that LTL with only past and no future modalities defines properties expressed over finite-words and these are the star-free subset of the regular languages. Standard LTL when ...

An excellent beginner overview is given by the following article from 2009. Boolean Satisfiability: From Theoretical Hardness to Practical Success, Sharad Malik, Lintao Zhang, Communications of the ...

Abstract interpretation is a very general concept and depending on whom you ask, you will receive different explanations because versatile concepts admit multiple perspectives. The view in this answer ...

Please read William Thurston's answer to the question What's a mathematician to do? on mathoverflow. Just to convince you that it is a must-read, let me quote him. The product of mathematics is ...

I briefly reviewed some areas here, trying to focus on ideas that would appeal to someone with a background in advanced mathematical logic. Finite Model Theory The simplest restriction of classical ...

There are different algorithms to convert regular expressions to finite automata. You can go directly from regular expressions to DFAs without building any other automaton first by implicitly doing ...

It's not a hidden link but one that has been made explicit using the language of category theory and also a very natural question to ask and study. There is a fair bit of material on the subject. CS ...

You are looking for an ALL-SAT or all solutions SAT solver. This is a different problem from #SAT. You do not have to enumerate all solutions to count them. I do not know of a tool that solves your ...

Lattices and fixed points are at the foundations of program analysis and verification. Though advanced results from lattice theory are rarely used because we are concerned with algorithmic issues such ...

(This started out as a comment and got way way way too long). You may enjoy William Thurston's article On Proof and Progress in Mathematics. Mathematics in some sense has a common language: a ...

Actually, I think what you're looking for is Kleene algebra. See Dexter Kozen's classic article. He gives an axiomatization of Kleene-star. I assume this is the very first step you're interested in. ...

Clarification on terminology The theorem proving community does not use the terms supervised and unsupervised. They use the terms interactive theorem proving or automated theorem proving. If you give ...

Here is a rather different application from what you may have had in mind. Linear programming has many practical applications. There are many algorithms for linear programming and those based on ...

The question you pose and the specific counting trick you describe is a classic one in program analysis. There is the theoretical problem of complexity analysis, and it's practical manifestation in ...

Turing's paper on Checking a large routine which was presented at a conference in Cambridge in 1949 antedates formal reasoning about programs as developed by Floyd and Hoare by nearly two decades. The ...

Shannon's source and channel coding theorems. A mathematical definition that distinguished between the transmitted, receiver and medium and which ignored the semantics of the message was a big step. ...

Not really an answer but the closest references I am aware of. There are results available for branch-width. Also, there is at least one empirical study of treewidth of industrial instances. ...

The motivation you state for dealing with undecidability applies to decidable but hard problems as well. If you have a problem that is NP-hard or PSPACE-hard, we will typically have to use some form ...

An important subclass of this family is a sub-class of 0-reversible languages. A language is 0-reversible if the reversal of the minimal DFA for the language is also deterministic. The reversing ...

This is more of a meta answer in that it is a list of lists. The papers of Doron Zeilberger. He is a mathematician and his computer is listed at the coauthor Shalosh B. Ekhad on all papers where the ...

There is a lot of work on Hoare Logic for object oriented programs, and for reasoning about memory allocation and deallocation. Some starting points: A Syntax-Directed Hoare Logic for Object-Oriented ...