TOC Seminar -- Kurt Sieber -- Tue., June 27

To: types@theory.LCS.MIT.EDU, logic@theory.LCS.MIT.EDU
Subject: TOC Seminar -- Kurt Sieber -- Tue., June 27
From: craig@theory.LCS.MIT.EDU
Date: Fri, 16 Jun 89 23:14:27 EDT
Sender: meyer@theory.LCS.MIT.EDU

Date: Fri, 16 Jun 89 11:13:24 EDT
To: theory-seminars@theory.LCS.MIT.EDU

			   DATE: Tuesday, June 27
			  TIME: Refreshments: 11am
			      Lecture: 11:15am
		     PLACE: Third Floor Conference Room

	 Reasoning about Sequential Functions via Logical Relations

				 Kurt Sieber
			   Universitat Saarbrucken

Traditional denotational semantics for programming languages is based on
cpo's and continuous functions.  But continuous functions can have
`non-sequential behavior', the simplest example for such a function is the
parallel or operator.  As a consequence, these continuous models are not
fully abstract for purely sequential languages.  The prototype for such a
language is PCF, a simply typed lambda-calculus with sequential if-then-else
and fixed point operators for all types.

Various approaches have been suggested to construct improved models which
only contain `sequential' functions.  Some of these constructions yield fully
abstract models for PCF, but they have a very syntactic flavor and don't help
us to reason about PCF-programs.  We present a new, purely semantic approach,
in which a particular set of logical relations is used to `cut down' the
continuous model.  Thus we obtain a new model for PCF which is fully abstract
for first order functions.  This already seems to be an improvement over
previous purely semantic approaches, which are either insufficient even for
the first order case (like stability) or can't be lifted to the whole type
hierarchy (like Kahn-Plotkin-sequentiality).  We expect that our result can
be extended to second order functions, for which we currently have a
`partial' full abstraction result (and a series of interesting examples).
Functions of order >= 3 have not yet been considered.

HOST: Prof. Meyer