[Prev][Next][Index][Thread]

paper announcement






The following two papers are available via anonymous ftp from
camille.is.s.u-tokyo.ac.jp in the directory /pub/papers.
A prototype interpreter of `hacl', a concurrent language based on 
linear logic programming, is also available via anonymous ftp from
camille.is.s.u-tokyo.ac.jp in the directory /pub/hacl.

Any comments are highly appreciated.

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

file name: oopsla94-type-coop-a4.ps.Z

    Type-Theoretic Foundations for Concurrent Object-Oriented Programing
                (to be presented at OOPSLA'94)
                              by
               Naoki Kobayashi and Akinori Yonezawa
       Department of Information Science, University of Tokyo

			Abstract

A number of attempts have been made to obtain type systems for object-oriented
programming. The view that lies common is
``{\em object-oriented programming = \(\lambda\)-calculus + record}."
Based on an analogous view ``{\em concurrent object-oriented programming
= concurrent calculus + record}," we develop a static type system
for concurrent object-oriented programming.
We choose our own Higher-Order ACL as a basic concurrent calculus,
and show that a concurrent object-oriented language can be easily encoded
in the Higher-Order ACL extended with record operations.
Since Higher-Order ACL has a strong type system with a polymorphic type 
inference mechanism, programs of the concurrent object-oriented language
can be automatically type-checked by the encoding in Higher-Order ACL.
Our approach can give clear accounts for complex mechanisms such as
inheritance and method overriding within a simple framework.


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

file name:  TR94-12-hacl-a4.ps.Z

     Typed Higher-Order Concurrent Linear Logic Programming
		(to be presented at TPPP'94, Sendai, Japan)
                        by
            Naoki Kobayashi and Akinori Yonezawa
       Department of Information Science, University of Tokyo

	                 Abstract

We propose a typed, higher-order, concurrent linear logic programming
called {\em higher-order ACL}, which uniformly integrates a variety of
mechanisms for concurrent computation based on asynchronous message
passing.  Higher-order ACL is based on a proof search paradigm
according to the principle, {\em proofs as computations}, {\em
formulas as processes} in linear logic.  In higher-order ACL,
processes as well as functions, and other values can be communicated
via messages, which provides high modularity of concurrent programs. 
Higher-order ACL can be viewed as asynchronous counterpart of Milner's
higher-order, polyadic \(\pi\)-calculus.  Moreover, higher-order ACL
is equipped with an elegant ML-style type system that ensures (1) well
typed programs can never cause type mismatch errors, and (2) there is
a type inference algorithm which computes a most general typing for an
untyped term.  We also demonstrate a power of higher-order ACL by
showing several examples of ``higher-order concurrent programming.''

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

Naoki Kobayashi
Department of Information Science
Faculty of Science
University of Tokyo
7-3-1 Hongo, Bunkyo-ku,
Tokyo 113, Japan
e-mail:koba@is.s.u-tokyo.ac.jp