compiler construction, programming language design, formal verification, proof automation, computational logic
