9 Jun 1989 20:04

### Summer school

Date: Fri, 9 Jun 89 15:53:47 BST
To: fp%information-systems.east-anglia.ac.uk@...,
types@...

Logic for IT'' Initiative and SERC sponsored Summer School on
FUNCTIONAL PROGRAMMING and CONSTRUCTIVE LOGIC

Kelvin Conference Centre, Glasgow, 17--23 September 1989

The programme will consist of five courses:

Polymorphic lambda calculus			Thierry Coquand
Calculus of constructions			Rod Burstall
Linear logic					Yves Lafont
Category theory and polymorphism		Philip Wadler
Category theory and abstract interpretation	John Hughes

together with several guest speakers and tutorial activities.  Some
time will be reserved for talks on more advanced research topics by
lecturers and attendees.  The school is organised by Philip Wadler,
Harold Simmons, and Martin Hyland.

This meeting aims to bring together and stimulate interaction between
the functional programming, category theory, and type theory
communities.  The lectures will be pitched at graduate students, young
lecturers, and established researchers in any one of these fields
who wish to learn about the other two.

There will be no charge for SERC-sponsored students.  For other
academic participants the total charge will be 250 pounds, and for


9 Jun 1989 20:06

### Summer school: errata

Date: Fri, 9 Jun 89 16:36:08 BST
To: fp%information-systems.east-anglia.ac.uk@...,
types@...

[Apologies.  The last paragraph of the previous message was missing
its second-to-last sentence.  Here is the corrected version.]

There are only a limited number of places available and these are
likely to be heavily oversubscribed.  Intending participants should
apply before 15 July to:

FPCL School
Department of Computing Science
University of Glasgow
Glasgow, G12 8QQ

or a cheque for the fee made out to FPCL School (if your are not).
Please do *not* respond by e-mail.


17 Jun 1989 05:14

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

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

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


17 Jun 1989 15:18

### Stability and Sequentiality

Date: Sat, 17 Jun 89 13:08:28 WET DST

apropos the MIT seminar announcement from craig@...
"Reasoning about Sequential Functions via Logical Relations" by Kurt Sieber

This already seems to be an improvement over
previous purely semantic approaches, which are either
insufficient even for the first order case (like stability)

Clearly the equation stable=sequential was wrong, as Berry himself
showed.  However this is not a reason for dismissing the idea of
stability in the analysis of sequential and parallel behaviour.
What is wrong with it is its use in a poset (qualitative) rather than
category (quantitative) setting.

Consider a program~$S$ consisting of several parallel processes
which merge their output indiscriminantly {\it without suppression of
duplication}; for instance parallel~or'' would output~${\bf t}$
{\it twice} on input $<{\bf t},{\bf t}>$. Suppose that on input~$X$ (a~bag
of tokens from~$A$) its output includes an instance~$Y=\{j\}$ of a
token~$j\in B$. This has come from a particular process, which itself
has pursued a {\it sequential} execution path, involving certain
hurdles'' which amount to reading and matching a  pattern~$X_0$ in~$X$;
moreover if~$X$ had contained only this pattern, $Y$~would still have
been output. The candidate is the function $u:Y\to SX_0$ which identifies
this instance of the token~$j$ in the output, but there may have been
many other ways in which this or other parallel processes could have
generated~$j$, but identified by different~$u$'s.

(Please excuse the TeX: this is an extract from my paper "Quantitative


17 Jun 1989 15:46

### Stability and Sequentiality

Below some recent email between Jim/Meyer, Berry, and Curien on the topic.
It seems Sieber's logical relations'' method for paring down
Scott-continuous models offers a general method similar in spirit to the
specific extensional compatibility'' repair Berry suggests below for avoiding
the counterexamples we note.
------------
---------
Date: Wed, 10 May 89 18:42:57 EDT
From: trevor@...
To: curien@..., jlevy <at> src.dec.com,
mcvax!inria.inria.fr!jlevy@...,
mcvax!inria.inria.fr!levy@...,
mcvax!mirsa.inria.fr!berry@..., meyer <at> theory.LCS.MIT.EDU

Recently we have been looking at models of PCF, in particular at the
very interesting stable function and also extensional sequential
algorithm models which you have developed.  It was neat to see how
these models restored the validity of Plotkin's counter-example to
full abstraction of Scott Domains for PCF.

But we were surprised to finally realize that the sense in which these
models meet the stated goal of your "State of the Art" paper--to be
"closer" to the fully abstract model of PCF--has not been clearly
achieved.  Namely, even though Plotkin's equation, which fails in the
Scott model, does indeed hold in the stable model, OTHER equations
which DO hold in the Scott model, fail in the stable model.

It doesn't seem fair to call the stable model "closer" than the Scott
model, since the equational theories of the two models are
set-theoretically incomparable.  This kind of incomparability appears


20 Jun 1989 18:03

### A sequential CCC?

Date: Tue, 20 Jun 89 16:33:28-0000

I tried to generalize the notion of sequential function and came up with
the definition below. Unfortunately it does not exclude the (counter)
examples Pierre-Louis Curien mentions in his monograph (e.g. the function
g minimal such that g(lor) = t and g(ror) = f), so I stopped working on
it. Recently however I think (think = you can never be sure with so many
indices floating around) I proved that the category is Cartesian closed.

SeqAlg II is the category with

objects <P,I,|.|> where

P is a partial order

I is a set (of indices or information quanta or something)

|.|  :  P --> 2^I  is a monotone function which, for every p in P,
gives the information required to calculate it

morphisms <f,{s_x}_x in P>  :  <P,I,|.|> --> <P',I',|.|'> where

f  :  P --> P'  is a continuous function

{s_x}_x in P  is a set of partial functions indexed by P with
s_x  :  I' \ |f(x)|'  -->  I \ |x|

f and {s_x}_x in P are connected in the following way:

s_x is defined at i in I' \ |f(x)|' iff there is a y > x


20 Jun 1989 19:43

### Feasible Math Workshop

Date:         Tue, 20 Jun 89 13:03:20 EDT

The Feasible Mathematics Workshop will be held
at Cornell University, Mon. June 26-28, under the
auspices of the Mathematical Sciences Institute,
organized by Sam Buss and Phil Scott.  A tentative
schedule is given below.
The "official motel" (= Collegetown Motor Lodge)
is now full, but an alternative motel,Best Western
(East Hill Plaza, Ithaca: 272-6100), has been recommended.
There are no registration fees, but you have to pay
some reasonable amount for banquet (to be determined).

FEASIBLE WORKSHOP

Sun., 25 June:  Party at Anil Nerode's House (evening)

Mon., 26 June:  9:00 Introduction
9:05-9:55  S. Cook
10:10-11:00  Blum
Coffee Break
11:25-12:15  Gurevich
LUNCH
2:00-2:50 Urquhart
Coffee Break
3:30-4:20 Crossley
4:35--4:55 : Contributed Talks.

Tues 27 June:   9:05-9:55 Girard
10:10-11:00 Scedrov


21 Jun 1989 01:55

### Semantics using ML

Date: Tue, 20 Jun 89 16:03:21 EDT

I am thinking about using ML in my "programming language theory"
course next fall to teach denotational semantics. Roughly, I am
tentatively planning to have students write semantic domains as
datatype definitions, semantic clauses as recursive functions
(pattern matching on constructors), and provide realistic program
syntac using the "yacc" feature. (This would follow an introduction
to typed lambda calculus and models; I don't want to give the idea
that denotational semantics is just a style of ML programming.)

Since this is such an obvious idea, I was wondering if anyone
"share" (as they say out here in CA).

John


21 Jun 1989 16:42

### Semantics using ML

Date: Tue, 20 Jun 89 22:22:16 -0400

I used ML as a semantic specification language for my PLT course.  It
worked quite well.  Semantic equations for Mike Gordon's Tiny and
Small are not difficult to write in ML and further extensions can be
assigned as exercises.  Allison's book "A practical introduction to
denotational semantics" could also be a usable source.  There is a
full ML denotational specification of a little Pascal-like language in
Huet's CMU lecture notes as well.

It would be handy to have exercises of this kind that made use of the
new Standard ML of New Jersey parser generator.

carl gunter


21 Jun 1989 23:08

### Semantics using ML

To: John C. Mitchell <jcm@...>
Cc: types@...

I am thinking about using ML in my "programming language theory"
course next fall to teach denotational semantics. ...

Since this is such an obvious idea, I was wondering if anyone
"share" (as they say out here in CA).

Perhaps it's a minor point, but having taught denotational semantics
in both T (a dialect of Scheme) and Alfl (a non-strict functional language
similar to SASL) I found the non-strict semantics of Alfl to facilitate the
teaching, for most of the standard reasons.  For example, in denotational
semantics we typically write things like:

E [[e0 where x = e1]] env = E [[eo]] env'
where env' = env[ E[[e1]]env' / x]

Note the recursive definition of env'.  In a functional language this
would look something like:

env' = update env "x" (E e1 env')

which in a strict language such as ML or Scheme would diverge, whereas
in a non-strict language such as Alfl, Miranda, or Haskell would not.
Of course, one can usually get around these problems in a strict language,
but there's something to be said for using the semantic equations almost
verbatim.  Thus I would recommend using Miranda, LML, or, if implementations
`