headers
Albert R. Meyer | 7 Jan 1988 18:03
Picon

[bemus-ac/9+7vlSMgK5/GGV6Q7qS32Wq3+S9qwWdbopdmp2Y19JmteYmzM1PQMNglOCcJ4QJKk+LtLqE5Eg3pRblZqziyWicD46zO2KMzqnlQLv9A=

PREVIEW OF POPL TALK:

Date: Wed, 6 Jan 88 16:10:28 est
From: Sally C. Bemus <bemus@...>
To: theory-seminars@...
Subject: TOC Seminar -- TOMORROW, January 7, 1987 -- Kurt Sieber

			DATE:    Thursday, January 7, 1987
			TIME:    Refreshments: 2:45PM
			LECTURE: 3:00PM
			PLACE:   NE43-512A

	    REASONING ABOUT LOCAL VARIABLES ALGOL-LIKE PROCEDURES

				 Kurt Sieber
			    Univ. des Saarlandes

We improve the usual denotational semantics for local variables to obtain a
"store-model" semantics which exactly captures (is "fully abstract for)
operational semantics of Algol-like procedures with first-order parameters
(call by reference).  Some simple facts about the behavior of local variables
in procedures with procedure parameters are then shown to be independent of
essentially all known program verification systems by observing that although
store models (1) agree with the operational semantics of completely declared
programs, and (2) all known proof rules for reasoning about programs are
sound for store models, nevertheless (3) some of the simple facts which are
true operationally are false on store models.  We then discuss methods for
constructing semantical models which justify stronger proof principles, using
various categories of functors into cpo domains.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Albert R. Meyer | 7 Jan 1988 18:03
Picon

[goguen-1VPwtPCARB3jDbLaPJHwntM38qrJMh250ST0WlP8WgjxJcQD/RG+/nvhT0Alu99NTb5A2QEG4//gxiamoUYe4Q==

To: fp@...
Cc: goguen@...
Subject: higher order functions considered unnecessary
Date: Tue, 05 Jan 88 18:58:28 -0800
From: goguen@...

I have just finished a paper which some of you might find amusing; the
abstract is appended below.  If you want a hardcopy, just send me a msg with
your hardcopy address.  Best wishes for the New Year to everyone on the list!
Cheers, Joseph

#########################################################################
Higher-Order Functions Considered Unnecessary for Higher-Order Programming
  Joseph A. Goguen

It is often claimed that the essence of functional programming is the use of
functions as values, i.e., of higher order functions, and many interesting
examples have been given showing the power of this approach.  Unfortunately,
the logic of higher order functions is difficult, and in particular, higher
order unification is undecidable.  Moreover (and closely related), higher
order expressions are notoriously difficult for humans to read and write
correctly.  This paper shows that typical higher order programming examples
can be captured with just first order functions, by the systematic use of
parameterized modules, in a style that we call *parameterized programming*.
This has the advantages that correctness proofs can be done entirely within
first order logic, and interpreters and compilers can be simpler and more
efficient.  A more subtle, but still important, point is that higher order
logic does not mix well with *order sorted logic*.  However, subsorts are very
useful in functional programming, since they support the clean and rigorous
treatment of partially defined functions, exceptions, overloading, multiple
(Continue reading)

Permalink | Reply | 0 comments |
headers
Paul Taylor | 20 Jan 1988 18:00
Picon

L-domains


Dear Polymorphic Colleagues!
   This is my first contribution to the "types" mailing list, so a
quick introduction first.  I was a student of Martin Hyland (in
Pure Maths) in Cambridge and completed my PhD, entitled

    Recursive Domains,  Indexed Category Theory and Polymorphism

in October 1986.  The main objective of this was the construction of
models of polymorphism (dependent types and Type:Type) in all then
existing categories of domains.  Wherever I could I worked with
continuous rather than algebraic domains, and had to develop a lot of
difficult ordinary domain theory in the process.  I concluded by
constructing a domain of "names" of domains with the property that any
dependent type A[x] had a dependent name n_A(x) such that T[n_A(x)] is
isomorphic to A[x].

   I am now interested in Berry-Girard domain theory and announce
the following (very recent) results of mine.  An "L-domain" is a
cpo in which every principal lower set is a continuous lattice
(the term, which I think should be replaced, is due to Achim Jung, who
has shown that if a cpo has algebraic function space then it is
either bifinite (SFP) or an L-domain).  I argue that "stable" should
mean all connected meets (codirected meets as well as pullbacks).
I can prove:

  (1)  The category of L-domains and stable maps is the category of
algebras for a monad defined over locally connected spaces/locales
or domains (not sets), the corresponding algebraic operations being
connected meets which distribute over directed joins.  cf Day [1975]
(Continue reading)

Permalink | Reply | 0 comments |
headers
Albert R. Meyer | 20 Jan 1988 18:02
Picon

NIKHIL@...

Date: Wed 20 Jan 88 13:54:45-EST
From: Rishiyur S. Nikhil <NIKHIL@...>
Subject: Miranda available
To: csg@...
Cc: ppg@..., mbr <at> XX.LCS.MIT.EDU

With Andy Boughton's help, I have installed Miranda on Newt.  This
version is the first ``official'' release (we had a pre-release
version before).

It has a fairly non-trivial system organization, including:
- a simple module organization, based on files
- compiled versions of source files, including automatic
  maintenance of consistency. (Compiled code = combinators,
  though I don't know what kind.)
- direct transfer between Miranda and a text editor (you can
  choose your editor, I have set the default to emacs)
- automatic recompilation of edited files
- reading, writing, appending to Unix files, including stdin, stdout,
   stderr, ...
- standalone Miranda programs (yes, you can write a Unix filter
   in Miranda)
- ``literate script'' convention, borrowed from the Oxford language
  OL.

To run Miranda, say

    mira

to newt's Unix shell prompt.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Albert R. Meyer | 21 Jan 1988 10:07
Picon

chlo@...

From: mcvax!doc.ic.ac.uk!chlo@...
Date: Wed, 20 Jan 88 14:48:01 GMT
To: meyer@...
Subject: Abramsky's Simulation ordering

Dear Professor Meyer,

You may certainly forward my comments on the distinctions between the 
simulation ordering and Bohm trees to TYPES.

Regards, Luke (Ong)
--------------------
From: mcvax!doc.ic.ac.uk!chlo@...
Date: Mon, 11 Jan 88 9:54:14 GMT
To: meyer@...
Subject: Abramsky's Simulation ordering

Dear Prof. Meyer,

With reference to the postscript you attached to Samson Abramsky's
e-mail dated 23 Nov, the ``simulation ordering'' M preord N
is not equivalent to two straight-forward modifications of
Bohm-tree ordering (to handle weak head normal forms) which
I have investigated. They are Longo tree ordering and weak Bohm
tree ordering. 

The former was introduced by Giuseppe Longo in his
'83 APAL paper (entitled ``Set-theoretic Models of Lambda-Calculus:
theories, expansions and isomorphisms''). Longo tree differs from
Bohm tree in that the former maps all strongly unsolvable terms
(Continue reading)

Permalink | Reply | 0 comments |
headers
Albert R. Meyer | 25 Jan 1988 22:16
Picon

NIKHIL@...

Date: Mon 25 Jan 88 19:34:05-EST
From: Rishiyur S. Nikhil <NIKHIL@...>
Subject: Your comments requested ...
To: csg@...

I have put together a document called ``Id Language Extensions''
outlining the proposed extensions to Id regarding algebraic types,
pattern matching, abstract types and syntax for lists, arrays and lazy
evaluation.  Copies are on the credenza in Susan's office.

Please look them over, and try them out on some of your Id programs, if you
can, and let us know your reactions.  Perhaps we can have a lively discussion
in Friday's group meeting, finalize the proposal and get started on
implementation.

Thanks.  Nikhil
-------
Permalink | Reply | 0 comments |
headers
John Mitchell | 26 Jan 1988 03:25
Picon

visiting professorship


Stanford has a visiting professorship which may be
awarded to a qualified applicant wishing to visit
for one or more quarters. (Quarters are approximately
10 weeks.) If anyone reading this list is interested,
please let me know as soon as possible. We will begin
reviewing applications on Feb 1.

John Mitchell
Permalink | Reply | 0 comments |
headers
Albert R. Meyer | 26 Jan 1988 19:53
Picon

Administrative Email to (Internet): types-request <at> theory.lcs.mit.edu

I'll be turning over email list maintenance to a staff member soon, so it
will be helpful if you henceforth send email on TYPES administrative
business---typically updating addresses---to
		      types-request@...
rather than me personally.  Thanks.

Regards, Albert
Moderator, types@...
Permalink | Reply | 0 comments |

Gmane