Overview
CLLT conducts pioneering research in type-theoretical approaches to natural language semantics, bridging formal linguistics and computational implementation. Our work demonstrates how modern type theories—particularly Martin-Löf Type Theory and Coq—can provide rigorous foundations for semantic analysis.
This research stream combines deep theoretical work with practical computational implementations, creating systems that are both mathematically rigorous and computationally executable.
Key Publications
Formal Semantics in Modern Type Theories
Chatzikyriakidis, S., & Luo, Z. (2020)
Comprehensive monograph on formal semantics using Modern Type Theories (MTT). Published by ISTE/Wiley Science, this work establishes MTT as a powerful framework for natural language semantics, covering compositionality, quantification, anaphora, and more.
Natural Language Inference in Coq
Bernardy, J.P., & Chatzikyriakidis, S. (2019)
Implementation of natural language inference using the Coq proof assistant. This work demonstrates wide-coverage symbolic NLI, providing executable formal semantics for reasoning tasks including the FraCaS test suite.
Collaboration with Leading Researchers
This research is conducted in collaboration with:
- Zhaohui Luo (Royal Holloway, University of London) - Modern Type Theories
- Jean-Philippe Bernardy (Chalmers/University of Gothenburg) - Coq implementations
- Robin Cooper (University of Gothenburg) - Type Theory with Records
Applications
Natural Language Inference
Symbolic NLI systems with provable correctness and explainable inference chains
Formal Verification of Semantics Theories
Formal verifications of formal semantics theories