Introduction

摘要

Type theory has been a central area of research in logic, the semantics of programming languages, and natural language semantics over the past fifty years. Recent developments in type theory have been used to reconstruct the formal foundations of computational semantics. The treatments are generally intensional and polymorphic in character. They allow for structured, fine-grained encoding of information across a diverse set of linguistic domains.