Formal Semantics in Modern Type Theories

6Reasoning and Verifying NL Semantics in Coq

We have so far been developing and studying MTT-semantics, the natural language (NL) semantics based on modern type theories (MTTs). One of the things that we have emphasized is that MTT-semantics is both model-theoretic and proof-theoretic. Being proof-theoretically presented, MTTs have been implemented in proof assistants, computer systems that have been developed by computer scientists for interactive development of proofs to prove mathematical theorems and to verify correctness of programs. Because MTT-semantics can be implemented straightforwardly in them, the proof assistants based on MTTs can be used effectively for reasoning (Luo 2011b; Chatzikyriakidis and Luo 2014, 2016).

In this chapter, we shall call this proof technology based on proof assistants as proof assistant technology and show how MTT-semantics can be implemented and how the semantic constructions studied in the previous chapters can be formalized and used to preform reasoning accordingly. We shall use the proof assistant Coq (Coq 2010), whose type theory pCIC is essentially the same MTT we have called UTT (Luo 1994) (see Chapter 2).¹ Therefore, one can think that we are using the impledicative type theory UTT in our Coq implementation of MTT-semantics and reasoning.

6.1. Proof assistant technology based on MTTs

Proof assistant technology has been studied since the early 1960s by people that were concerned with the formalization of mathematics, i.e. interactive ...