@inproceedings{raaijmakers-1993-proof,
    title = "A Proof-Theoretic Reconstruction of {HPSG}",
    author = "Raaijmakers, Stephan",
    editor = "Bunt, Harry  and
      Berwick, Robert  and
      Church, Ken  and
      Joshi, Aravind  and
      Kaplan, Ronald  and
      Kay, Martin  and
      Lang, Bernard  and
      Nagao, Makoto  and
      Nijholt, Anton  and
      Steedman, Mark  and
      Thompson, Henry  and
      Tomita, Masaru  and
      Vijay-Shanker, K.  and
      Wilks, Yorick  and
      Wittenburg, Kent",
    booktitle = "Proceedings of the Third International Workshop on Parsing Technologies",
    month = aug # " 10-13",
    year = "1993",
    address = "Tilburg, Netherlands and Durbuy, Belgium",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/ingest-emnlp/1993.iwpt-1.19/",
    pages = "235--256",
    abstract = "A reinterpretation of Head-Driven Phrase Structure Grammar (HPSG) in a proof-theoretic context is presented. This approach yields a \textit{decision procedure} which can be used to establish whether certain strings are generated by a given HPSG grammar. It is possible to view HPSG as a fragment of linear logic (Girard, 1987), subject to partiality and side conditions on inference rules. This relates HPSG to several categorial logics (Morrill, 1990) . Specifically, HPSG signs are mapped onto quantified formulae, which can be interpreted as \textit{second-order} types given the Curry-Howard isomorphism. The logic behind type inference will, aside from the usual quantifier introduction and elimination rules, consist of a partial logic for the undirected implication connective. It will be shown how this logical perspective can be turned into a parsing perspective. The enterprise takes the standard HPSG of Pollard {--} Sag (1987) as a starting point, since this version of HPSG is well-documented and has been around long enough to have displayed both merits and shortcomings; the approach is directly applicable to more recent versions of HPSG, however. In order to make the proof-theoretic recasting smooth, standard HPSG is reformulated in a binary format."
}