headers
meyer | 6 Jan 1989 15:33
Picon

Semantics Lectures at IBM Yorktown

This is a preliminary announcement; full version with titles and abstracts to
appear on TheoryNet.
------------------
              The Programming Languages and Foundations Department
                    of the IBM  T.J. Watson Research Center

              Announces a series of distinguished lectures on the

                       SEMANTICS OF PROGRAMMING LANGUAGES

          ------------------------------------------------------------
          January  26         Albert Meyer, MIT

   TITLE:  An Ultimate ``Kahn Principle'' for Dataflow Semantics

   ABSTRACT: Kahn showed in the mid-70's that dataflow nets whose nodes process
   inputs ``sequentially'' AND ``functionally'' can be analyzed by fixed-point
   reasoning on the domain of data-streams.  On the other hand, Brock-Ackermann
   observed in the late 70's the ``anomaly'' that for nondeterministic nodes
   such as MERGE, the data-stream input-output behavior of the nodes did not
   even uniquely determine the behavior of nets using such nodes.

   We report on some notable progress on the mathematical semantics of dataflow
   nets made recently by independent groups at Tel Aviv, MIT, and Cornell.  For
   example, Kahn's Least-Fixed Point Principle can now be extended to nets with
   non-sequential functional nodes, and Brock-Ackermann's anomaly can be culled
   from essentially any nonfunctional nodes.  This case study also illustrates
   the significance of such basic concepts in programming semantical as
   compositionality, observational congruence, and full abstraction.
(Continue reading)

Permalink | Reply | 0 comments |
headers
John Mitchell | 22 Jan 1989 01:07
Picon

Kripke lambda models

Date: Sat, 21 Jan 89 15:35:18 PDT
To: meyer@..., riecke <at> theory.LCS.MIT.EDU
Cc: types@...

This is a response to "point 3" of a message about Kripke
lambda models from Jon Riecke and Albert Meyer.
The point they raises was essentially that it followed in the
framework of my paper with Moggi in 1987 LICS (to appear in
J. Pure and Applied Logic one of these days) that
if T is the first-order theory of a class of Kripke lambda models 
(regarded as multi-sorted  first-order structures), then T is the 
theory of a single Kripke model. Here is a summary of some relevant
communication (to bring everyone up to date, and remind Meyer
and Riecke what we were discussing), follows by my current
point of view.

JCM:
   Date: Fri, 6 Jan 89 15:54:44 PDT
   From: John Mitchell <jcm@...>

   I can't see why 3. would be true, for much the same
   reasons that it fails for classical models. (We have
   disjunction in first order logic, so a disjunction
   of closed formulas may hold for a class of models
   without either disjunct holding for the entire class.)
   What did I/we say that suggested 3. is true?

RIECKE:
We suspected 3 might hold from an informal statement made on page 313 in your
paper:
(Continue reading)

Permalink | Reply | 0 comments |
headers
lcp%computer | 24 Jan 1989 15:20
Picon
Picon

well-founded induction

Date: Tue, 24 Jan 89 09:30:57 GMT
To: TYPES@...

Is it practical to use a formal derivation of well-founded induction in
Church's higher-order logic?  E.g. define (with the obvious type symbols)

    WF(>) = there is no f such that for all n,  f(n)>f(n+1)

Then from the premises of wf induction

    WF(>)       forall x ( (forall y  x>y --> P(y))  -->  P(x) )

and the negated conclusion ~P(z) it follows that for some z1, z>z1 and ~P(z1),
and so on.  Use Hilbert's epsilon to define f.  Perhaps induction over the
naturals has to be assumed.

Is the full construction presented anywhere?

Larry
Permalink | Reply | 0 comments |
headers
Paul Taylor | 25 Jan 1989 16:54
Picon
Picon

CCCs of Stable Domains

Date: Tue, 24 Jan 89 18:52:57 GMT
To: types@...

			The Trace Factorisation
			 and Cartesian Closure
			 for Stable Categories

In August I advertised on "types" that I had proved that the following
2-category is cartesian closed:
   objects:  locally small categories with small filtered colimits
	and a set of objects of which from which any object can be
	constructed using filtered colimits, such that every slice
	category [is a continuous category in the sense of Johnstone-Joyal]
	[is complete, and filtered colimits are preserved by pullbacks].
   morphisms: functors preserving filtered colimits, which on every
	slice have left adjoints
   2-cells: cartesian natural transformations
This is a substantially larger 2-category than those studied by Berry,
Girard, Coquand-Gunter-Winskel, Coquand, myself and Lamarche.

Several people requested copies of my work then; I confess I have a
bad reputation for supplying copies, but
I HAVE NOW COMPLETED (ALMOST ALL OF) THE PROOF AND AM MAKING COPIES
FOR DISTRIBUTION THIS EVENING.

The paper begins with a discussion of diagonal universality, which
generalises the well-known idea of a "universal map from an object
to a functor" (one of the ways of saying the functor has a left
adjoint). This is developed into the trace factorisation, and it
is shown that many examples from Girard and Diers fit into this
(Continue reading)

Permalink | Reply | 0 comments |
headers
Philip J. Scott | 26 Jan 1989 00:04
Picon

Feasible Mathematics Workshop

Date:         Wed, 25 Jan 89 14:32:54 EST

To: types@...

                  FEASIBLE MATHEMATICS WORKSHOP
   Analyzing complexity of algorithms is both a practical
problem and a major area of theoretical research for computer
scientists, logicians, and mathematicians.  Since the 1960's,
there has been an increasingly sophisticated classification
of algorithms into natural classes (e.g. P, NP, P-Space, Exp-time,
etc.) leading to a deeper understanding of the limits of feasible
computation.
    More recently, researchers have begun investigating the logical
and mathematical consequences of "resource-bounded" (e.g. polynomial
time) mathematics. Active areas include:  polynomial-time logics,
bounded versions of arithmetic and lambda calculus, proof theory
of feasible systems, feasible polymorphic languages, and polynomial
time versions of algebra and analysis.  Such "feasible" mathematics
typically mixes logical techniques from proof theory and finite model
theory, as well as complexity and recursion theory, combinatorics,
and traditional mathematics.
   There will be a Workshop from June 26-28, 1989 to be held at
Cornell University, under the auspices of MSI (Anil Nerode, Director),
entitled " Feasible Mathematics".
    This workshop will gather together researchers from various
disciplines to discuss the state of the art in this area.
Researchers who are currently scheduled to speak include:  M. Ajtai,
L.Blum, S.Buss, P. Clote, J. Crossley, S. Cook, J-Y.Girard, Y. Gurevich,
K-I Ko, D. Leivant, A. Nerode, J. Remmel, A. Scedrov, P. Scott,
G. Takeuti, and A. Urquhart.
(Continue reading)

Permalink | Reply | 0 comments |
headers
meyer | 28 Jan 1989 00:08
Picon

archives of messages

My machine on internet
			     theory.lcs.mit.edu

now supports anonymous login, so I have made available for ftp'ing recent
archives of the TYPES, CONCURRENCY, and LOGIC (in Computer Science) messages
of the past six or eight months.  They are in EMACS RMAIL format and will
updated and available from now on.

They can be found in the directory
			      /u/ftp/pub/meyer

Yours truly,
Prof. Albert R. Meyer
MIT Lab. for Computer Science
Moderator, TYPES@..., CONCURRENCY <at> theory.lcs.mit.edu,
	LOGIC@...
Permalink | Reply | 0 comments |
headers
meyer | 28 Jan 1989 00:08
Picon

archives of messages

My machine on internet
			     theory.lcs.mit.edu

now supports anonymous login, so I have made available for ftp'ing recent
archives of the TYPES, CONCURRENCY, and LOGIC (in Computer Science) messages
of the past six or eight months.  They are in EMACS RMAIL format and will
updated and available from now on.

They can be found in the directory
			      /u/ftp/pub/meyer

Yours truly,
Prof. Albert R. Meyer
MIT Lab. for Computer Science
Moderator, TYPES@..., CONCURRENCY <at> theory.lcs.mit.edu,
	LOGIC@...
Permalink | Reply | 0 comments |
headers
Ray Hirschfeld | 29 Jan 1989 04:26
Picon

archives of messages

Date: Sat, 28 Jan 89 17:02:21 EST

To: meyer@...
In-Reply-To: meyer@...'s message of Fri, 27 Jan 89
18:08:58 EST <8901272308.AA11518 <at> stork.LCS.MIT.EDU>

One thing you should point out to your subscribers is that from the
point of view of an anonymous ftp login, the directory is /pub/meyer,
not /u/ftp/pub/meyer.  Anonymous ftp does a chroot to /u/ftp for
security--nothing outside of /u/ftp is accessable.  See "man chroot".

				Ray
Permalink | Reply | 0 comments |
headers
Baiba Menke | 31 Jan 1989 21:16
Picon

CRCT Colloquium, 2/9, Semantic Interpretation

Date: Tue, 31 Jan 89 15:08:10 EST
To: colloquium@..., cs-gradstudents <at> harvard.harvard.edu,
        cs_ecse-faculty@...,
        cs_ecse-srfaculty@..., msgs <at> harvard.harvard.edu

				 COLLOQUIUM

	      Semantic Interpretation as Constrained Deduction

			   Fernando C. N. Pereira
		       Artificial Intelligence Center
			      SRI International

			 Thursday, February 9, 1989
				    4  PM
		      Aiken Computation Laboratory 101
		    (Tea at 3:30 pm Aiken Basement Lobby)

Abstract
Several recent approaches to semantic interpretation for natural
language use specialized deductive systems to specify how the meaning
of a phrase is built from the meanings of its constituents.  These
systems extend the notion of compositionality in important ways to
provide for proper treatments of quantification, bound anaphora, and
certain interactions between semantic and pragmatic phenomena.  I will
discuss two particular instantiations of these ideas. The first is
embodied in a natural language system (constructed collaboratively
with Martha Pollack) for building descriptions of maintenance
procedures, and provides basic treatments of the above phenomena. The
second is an attempt to remedy certain problems that were identified
(Continue reading)

Permalink | Reply | 0 comments |

Gmane