Constructive semantics for extensional PTQ

In this paper, the syntax and semantics for a fragment of English is provided within the framework of Martin-Lof´s type theory. The first to explore the potential benefits of this application was Aarne Ranta (1991). The motivation for the present work is to develop more traditional approach (Montague-style semantics) to semantics based upon the constructive framework. The work is focused on the parsing problem, which consists of providing the interpretation of a given English sentence as an expression in the type theory. In this paper it is shown that the parsing and semantic interpretation of a sentence can be accomplished in a compositional fashion by defining semantic rules that work in a one-to-one correspondence with the syntactic ones.