Research in the LFCS in the area of Logic and Proof is concerned with developing foundational theories with underpin computation, and with developing effective computer support for development of proofs in these theories from both a mathematical and computational perspective. Current theoretical interest is in such areas as constructive mathematics, type theory, category theory, linear logic and logical frameworks. Implementation effort is focused through the Lego proof system, a state-of-the-art proof assistant which supports the mathematician or computer scientist in the development of formal proofs. Lego has been used to develop substantial machine checked theories in mathematics and computation theory.
| Rod Burstall |