Using Type Theory with Records for HPSG

I will show how HPSG like grammars can be represented in type theory
with records.  This is part of an ongoing project using a version of
type theory based on Martin-Löf or constructive type theory to give an
account of semantics and syntax incorporating Montague semantics,
discourse representation theory, situation semantics and HPSG into a
single framework.  In this paper we will give an informal introduction
to the type theory we are using.  We will then consider some classical
cases of unification involving agreement and show how they can be
recast in terms of typing exploiting the kind of subtyping introduced
by records.  We will then explain why semantics needs notions like
functions and binding rather than unification.  We will show how a
unification-based approach to semantic representation can lead to
problems in cases where we need to refer to the interpretation of
subconstituents of a constituent and illustrate this with the
representation of information structure.  We will show that the
problem does not arise in a type theoretic approach.  Finally, if
there is time, we will consider how the computer science notions of
abstract and concrete syntax (exploited by Aarne Ranta in his
Grammatical Framework) might be imported into this framework and how
the result might cast illumination on the relationship between HPSG
and LFG.