Logic and Foundations

This group gathers pioneers of theory of computation whose primary contribution was mathematical logic and the foundations of computing, including Boolean algebra, set theory, Godel incompleteness theorems, proof theory and model theory, type theory and category theory, and the semantics of programs through denotational semantics, Hoare logic and formal program verification. It follows the Logic and the Semantics and reasoning second-level headings of the ACM Computing Classification System under Theory of Computation. Their shared work is the logical and mathematical bedrock computation rests on and the formal proof that a program meets its specification, as distinct from an algorithm running time, which belongs to Algorithm Design and Analysis, or a machine expressive power, which belongs to Formal Languages and Automata Theory.