recursively typed lambda calculus

• To: types@dcs.gla.ac.uk
• Subject: recursively typed lambda calculus
• From: mueller@cs.uni-sb.de (Fritz Mueller)
• Date: Mon, 5 Jul 93 14:41:26 +0200
• Approved: types@dcs.gla.ac.uk

Full Abstraction for a Recursively Typed Lambda Calculus
with Parallel Conditional,
by Fritz M"uller, Universit"at des Saarlandes.

A copy of this report is available by snail mail from the author,
send your address to  mueller@cs.uni-sb.de

Abstract:

We define the syntax and reduction relation of a recursively typed
lambda calculus with a parallel case-function (a parallel
conditional).  The reduction is shown to be confluent.  We interpret
the recursive types as information systems in a restricted form, which
we call prime systems. A denotational semantics is defined with this
interpretation. We define the syntactical normal form approximations
of a term and prove the Approximation Theorem: The semantics of a term
equals the limit of the semantics of its approximations. The proof is
by the inclusive predicate technique. The semantics is adequate with
respect to the observation of boolean values. It is also fully
abstract in the presence of the parallel case-function.

• Prev: OOL paper available by anonymous ftp
• Next: Full ILL paper
• Index(es):
  • Main
  • Thread