Research Grants

• EUTypes COST grant
• HoTT-based Computer-Assisted Reasoning (Royal Academy of Engineering)
• Lexical Semantics in Type Theory with Coercive Subtyping (Leverhulme Trust)
• Pythagoras: Machine support for semi-formalised proof oriented mathematics (UK EPSRC)
• Type-theoretic foundation of mathematical pluralism (Leverhulme Trust)
• TYPES Working Group (EU Framework VI)
• Reverse mathematics in dependent type theory (Robin Adams' fellowship from EPSRC)
• Epigram: Innovative Programming via Inductive Families (UK EPSRC)
• An open proof checker based on type theory (UK EPSRC)
• Subtyping, inheritance, and reuse: developing expressive type theory for formal analysis (UK EPSRC)
• Computer-assisted reasoning with natural language: implementing a mathematical vernacular (Leverhulme Trust)
• TYPES WG (EU Framework V; coordinator)