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.
Related Links
- Logic and Semantics Seminars. This is our main group seminar series, and takes place most Fridays during term time. It is currently held online.
- Semantics Lunch. This informal lunch meeting gives a venue for PhD students to present their research.
- Programming, Logic, and Semantics Group. This is the old group page for the Programming languages, compilers, and analysis; development and application of automated reasoning tools; mathematical models of hardware, software, and networks; finite model theory
- Rigorous Engineering of Mainstream Systems. The homepage for the REMS project.
- Automated Reasoning Group. The ARG studies logical techniques for computational reasoning.
- Cambridge Logical Structures Hub (CLASH). Research group focusing on logical and structural techniques in the foundations of computer science, including type theory, category theory, mathematical logic and model theory.
