Formalization of Contexts in Type Theory with Records and Modules

Traditional type-theoretical semantics lacks convenient instruments for taking into account contextual information. To cope with this deficiency, a type theory with records was proposed by Robin Cooper. However, it possesses limited capacities as to the formalization of such phenomena as the referential opacity of contexts. At the same time, a lot of functional programming languages based on type theory contain sophisticated module systems providing means for opening or hiding various information from one or another fragment of programs. This article deals with opportunities that type theory with records and modules opens for the formalization of contexts in natural language semantics. The formalization is implemented in the dependently typed functional language Agda. Using programming language for type-theoretical semantics is not without a reason. Type theory is closely connected not only to logic, but also to computing, and programming in particular. In the context of type-theoretical semantics, we can understand meaning as something computable. That is why many semantic problems turn out to be connected with the development of methods (and programs) of meaning or referent calculation. The article outlines basic principles of formalization and its specific realization in Agda. Relation to situation semantics by Jon Barwise and John Perry is demonstrated. Examples of descriptions for contexts' referential opacity as well as the concepts of abstract meaning and meaning-in-use from situation semantics are provided. The Agda formalization code is freely available.

Keywords

Authors

References