Programming languages, compilers, and analysis; development and application of automated reasoning tools; mathematical models of hardware, software, and networks; finite model theory
Research in the Programming, Logic, and Semantics group is centred around the study of programming languages, logics, and mathematical models, addressing hardware, software, and networks. It spans a wide range of applied and theoretical work: programming language design, compilers, and program analysis; the development of interactive theorem provers and automatic proof procedures; the formal verification of computational systems; and semantic models using techniques such as structural operational semantics, type systems, domain theory, category theory, finite model theory and linear logic. Work is in progress on the underlying mathematical structures of these, and on their application to the study of higher-order typed programming languages; object-based languages; low-level machine languages; foundational languages for concurrent, distributed and mobile computation; hardware description languages; security and networking problems; database theory; and computational complexity.