@device(postscript)
@libraryfile(Mathematics10)
@libraryfile(Accents)
@style(fontfamily=timesroman,fontscale=11)
@pagefooting(immediate, left "@c<Technical Report 1996>",
center "@c<Computer Science>",
right "@c<Carnegie Mellon>")
@heading(Primitive Recursion for Higher Order Abstract Syntax)
@heading(CMU-CS-96-172)
@center(@b(Joelle Despeyroux@foot<Currently with INRIA, F-06902 Sophia-Antipolis Cedex, France>, Frank Pfenning, Carsten Schurmann))
@center(August 1996)
@center(FTP: CMU-CS-96-172.ps.gz)
@blankspace(1)
@begin(text)

Higher-order abstract syntax is a central representation technique in
logical frameworks which maps variables of the object language into
variables in the meta-language.  It leads to concise encodings, but is
incompatible with functions defined by primitive recursion or proofs by
induction.

In this paper we propose an extension of the simply-typed
lambda-calculus with iteration and case constructs which preserves the
adequacy of higher-order abstract syntax encodings.  The well-known
paradoxes are avoided through the use of a modal operator which obeys
the laws of S4.  In the resulting calculus many functions over
higher-order representations can be expressed elegantly. Our central
technical result, namely that our calculus is conservative over
the simply-typed lambda-calculus, is proved by a rather complex argument
using logical relations.

We view our system as an important first step towards allowing the
methodology of LF to be employed effectively in systems based on
induction principles such as ALF, Coq, or Nuprl, leading to a synthesis
of currently incompatible paradigms.


@blankspace(2line)
@begin(transparent,size=10)
@b(Keywords:@ )@c<Modal lambda caculus, higher order abstract syntax,
primitive recursion>
@end(transparent)
@blankspace(1line)
@end(text)
@flushright(@b[(119 pages)])