Type theory with records is a formal semantics representation framework, using records to express type theory types. It has been used in natural language processing, principally computational semantics and dialogue systems.

## Syntax

A record type is a set of fields. A field is a pair consisting of a label and a type. Within a record type, field labels are unique. The witness of a record type is a record. A record is a similar set of fields, but fields contain objects instead of types. The object in each field must be of the type declared in the corresponding field in the record type.

Basic type: ${\begin{bmatrix}{\text{x)):Ind\end{bmatrix))$ Object: ${\begin{bmatrix}{\text{x))=a\end{bmatrix))$ Ptype: $\left[{\begin{array}{lll}{\text{x))&:&Ind\\{\text{c))_{\text{boy))&:&boy({\text{x)))\\{\text{y))&:&Ind\\{\text{c))_{\text{dog))&:&dog({\text{y)))\\{\text{c))_{\text{hug))&:&hug(x,y)\end{array))\right]$ Object: $\left[{\begin{array}{lll}{\text{x))&=&a\\{\text{c))_{\text{boy))&=&p_{1}\\{\text{y))&=&b\\{\text{c))_{\text{dog))&=&p_{2}\\{\text{c))_{\text{hug))&=&p_{3}\end{array))\right]$ where $a$ and $b$ are individuals (type $Ind$ ), $p_{1)$ is proof that $a$ is a boy, etc.

1. ^ Cooper, Robin (2005). "Records and Record Types in Semantic Theory". Journal of Logic and Computation. 15 (2): 99–112. doi:10.1093/logcom/exi004.
2. ^ Cooper, Robin (2010). Type theory and semantics in flux. Handbook of the Philosophy of Science. Volume 14: Philosophy of Linguistics. Elsevier.
3. ^ R. Cooper. Type theory and language: From perception to linguistic communication. Draft of book chapters available from https://sites.google.com/site/typetheorywithrecords/drafts