Type Theory and Applications

Type Theory and Applications

Type Theory and Applications

We work on type theory and its applications, including:

Development of type theories
Computer-assisted proof development
Verification of programs
Formalisation of mathematics
Advanced issues in programming
Linguistic semantics

The current members of the research group are (list of previous members can be found here):

Dr. Stergios Chatzikyriakidis
Georgiana Lungu
Prof Zhaohui Luo
Fedor Part

The current research projects include:

Lexical Semantics in Type Theory with Coercive Subtyping (Leverhulme Trust)
HoTT-based Computer-Assisted Reasoning (Royal Academy of Engineering)

TYPES consortium and conference series:

TYPES conference series