[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