Resent-Message-Id: <199312201858.AA03137@theory.lcs.mit.edu>
From: "David M. Jones" <dmjones@THEORY.lcs.mit.edu>
Subject: TACS'94: Invited Lectures and Special Lectures
Date: Thu, 16 Dec 93 16:07:56 EST
To: theorynt@vm1.nodak.edu, logic@cs.cornell.edu, concurrency@cwi.nl
Old-Resent-From: types-request@dcs.gla.ac.uk
Errors-To: types-request@dcs.gla.ac.uk
Approved: types@dcs.gla.ac.uk
Resent-Date:  Fri, 17 Dec 1993 17:30:27 +0000
Resent-From: types@THEORY.lcs.mit.edu
Resent-To: types-dist@THEORY.lcs.mit.edu
Message-Id:  <9312190344.aa11837@MINTAKA.LCS.MIT.EDU>


A few days ago we broadcast the conference program and registration
material for the TACS'94 conference.  Here is some additional
information about the conference, namely, titles and abstracts for the
invited talks and special lectures that will be presented at the
conference.

Further information about the conference or a copy of the registration
material can be obtained at the following addresses:

 Email: tacs94@ito.ecei.tohoku.ac.jp
 Fax:   +81 22 267 4404
 Postal Address:
         Prof. Takayasu Ito, TACS'94 Co-Chair 
         Dept. Computer and Mathematical Sciences
         Graduate School of Information Sciences
         Tohoku Univ. [Aobayama Campus]
         Sendai 980, Japan


     "INVITED TALKS" AND "TACS SPECIAL OPEN LECTURES" AT TACS'94
     ===========================================================

                   List of Invited Talks at TACS'94

---------------------------------------------------------------------------

Samson Abramsky (Imperial College, London)

Full Abstraction for PCF
(Joint work with Radha Jagadeesan and Pasquale Malacaria)

The full abstraction problem for PCF is one of the best-known and
longest standing problems in the semantics of computation. It concerns
the semantic characterization of sequential, functional computation at
higher types, and holds (part of) the key to the proper understanding
of many important programming mechanisms.

This problem has recently been solved by the author and his
colleagues, using tools from game semantics and Linear logic. The
background and history of the problem, and the key ingredients of the
solution, will be described.

-----------------------------------------------------------------------------

Paris Kanellakis (Brown University)

Constraint Programming and Database Query Languages

Constraint programming languages provide the natural declarative
paradigm that generalizes Codd's relational data model and query
languages. We will discuss the expressive power and the efficiency of
various constraint query languages.

-----------------------------------------------------------------------------

Matthias Felleisen (Carnegie-Mellon University)

Extensible Denotational Language Specifications

The talk will introduce a style of denotational data type
specifications and interpreters that can be uniformly extended to cope
with new features. For example, in traditional semantics, the
denotation of a numeral changes from Env -> N (direct style) to Env ->
Continuation -> N (cps style) or Env -> State -> State x N (state
pasing style). In our framework, the denotation of a number will
always be the injection of a number into the value domain. It is thus
possible to prove that the denotations of old phrases are always
projections of their new denotations--even if we do NOT know what the
extensions are. It is also possible to combine interpreters by
basically juxtaposing them.

-----------------------------------------------------------------------------

Akinori Yonezawa (University of Tokyo)

Theory and Practice in Concurrent Object-Oriented Computing

This talk gives an overview of the progress in research on Concurrent
Object-Oriented Computing both in theory and practice. From the
theoretic standpoint, the developments of semantics bases for
concurrent object-oriented languages are focused; Calculi, computation
models, and type systems based on various frameworks such as rewriting
systems, linear logic etc are overviewed.  >From the practical
standpoint, the latest development of implementation technologies for
concurrent object-oriented languages on massivley parallel computers
is summarized.

-----------------------------------------------------------------------------

Masako Takahashi (Tokyo Institute of Technology)

Normal Proofs and Their Grammar
(joint work by M.Takahashi, Y.Akama, and S.Hirokawa)

In this work, we discuss grammatical descriptions of the sets { M in
normal form | Gamma |- M : A } (for bases Gamma and types A in the
simple type system), and its applications to typed/untyped
lambda-calculi. For example, we prove Berardi's conjecture on the
coding of untyped lambda-terms by means of simply typed lambda-terms.

-----------------------------------------------------------------------------

Moshe Vardi (IBM Almaden Research Center)

Nontraditional Applications of Automata Theory

Finite-state automata have two traditional applications in computer
science: description of regular set of finite strings and modeling of
finite-state systems.  In the last few years, several new applications
for finite-state automata have emerged, e.g., specification and
verification of protocols and optimization of logic programs.  These
applications use finite-state automata to describe regular sets of
trees and of infinite strings.  The speaker will describe such
applications and will argue that we need change the way we teach
automata theory.

-----------------------------------------------------------------------------

Zohar Manna (Stanford University)

Temporal Verification Diagrams

We use Diagrams as a tool for the verification of temporal properties
of reactive, real-time ,and hybrid systems.

=============================================================================

                  List of TACS Special Open Lectures

-----------------------------------------------------------------------------

John Mitchell (Stanford University)

Type systems and the design of object-oriented languages

Object-oriented programming languages and user-interfaces have
received increasing attention over the past decade.  Two important
features of these languages are subtyping, which allows objects of one
type to be used in place of objects of another, and inheritance, which
allows significant code reuse during program development. This talk
will summarize aspects of object-oriented languages that appear to be
important in practice and summarize several trade-offs in programming
language design. These included the choice to separate implementations
from interfaces, which is useful in system design but raises problems
with the implementation of typed binary operations, and whether
subtyping should be tied to the inheritance hierarchy or inferred
separately.  We will look at several recent type-theoretic approaches
to object systems and suggest directions for future research.

-----------------------------------------------------------------------------

Albert R. Meyer (MIT Laboratory for Computer Science)

Observing Truly Concurrent Processes

``Interleaving'' theories of concurrent processes such as CCS, CSP,
ACP, and pi-calculus, specify the state-transition behavior of
processes.  ``True'' concurrency models such as Petri Nets, and true
concurrency semantics such as pomset-processes, are needed in
situations requiring distinctions among processes with the same state
behavior, for example

** when a process observer can detect the simultaneous occurrence of
   two atomic actions,

** when an action may be interrupted by another process,

** when analysis of degree of parallelism (number of ``threads'') is
   desired.

We review several proposed true concurrency semantics, consider their
connection to a Petri Net computational model, and examine how
distinctions based on true concurrency can be detected by a purely
sequential observer.