[Prev][Next][Index][Thread]
Re: PER's and operational semantics
To: gunter@saul.cis.upenn.edu
Cc: types@theory.lcs.mit.edu
In-Reply-To: Your message of Fri, 21 Sep 90 13:09:39 -0400.
<9009211709.AA07500@stork>
Reply-To: John C. Mitchell <jcm@cs.stanford.edu>
Date: Fri, 21 Sep 90 11:46:56 -0700
Sender: jcm@iswim.stanford.edu
This is a reasonable question. There are several situations you might
take a look at. The simplest, which might not turn out to be very
interesting, is traditional HEO as a model of typed lambda calculus,
perhaps with primitive recursion operators at all types. Since all of
the recursive functions in this model are total, some of the issues
ordinarily involved in establishing computational adequacy might not arise.
A more interesting question, to my mind, is what happens with models that
do contain a fixed-point operator, and the relationship between the
domain structure and recursion theory. The papers in Session 11 of last
LICS might be a good place to start here (Freyd Mulry Rosolini Scott;
Abadi Plotkin; Phoa). Perhaps this is what you were suggesting, Carl,
when you asked about the untyped rather than typed calculus?
John