headers
Philip Wadler | 9 Jun 1989 20:04
Picon

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Philip Wadler | 9 Jun 1989 20:06
Picon

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

Send your name, address, phone number, e-mail address (if any), and
your SERC research student number (if your are a SERC-sponsored student)
or a cheque for the fee made out to FPCL School (if your are not).
*Please include one paragraph on your background and interests.*
Please do *not* respond by e-mail.
Permalink | Reply | 0 comments |
headers
craig | 17 Jun 1989 05:14
Picon

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Paul Taylor | 17 Jun 1989 15:18
Picon

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
meyer | 17 Jun 1989 15:46
Picon

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Andreas Knobel | 20 Jun 1989 18:03
Picon

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Philip J. Scott | 20 Jun 1989 19:43
Picon

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
John C. Mitchell | 21 Jun 1989 01:55
Picon

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
had tried this before, and had any advice or software to
"share" (as they say out here in CA).

John
Permalink | Reply | 0 comments |
headers
Carl Gunter | 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
Permalink | Reply | 0 comments |
headers
Paul Hudak | 21 Jun 1989 23:08
Picon
Favicon

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
    had tried this before, and had any advice or software to
    "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 
are available in time, Haskell.
(Continue reading)

Permalink | Reply | 0 comments |

Gmane