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

Summary: object-oriented type systems in practice



Last week, I sent out the following request:

> I received the following request from Roy Ju of Intel's Compilers and
> Java Lab:
> 
> > We would like to understand a wide spectrum of the issues under type
> > safety, but a few examples of what we have in mind are security in
> > sharing objects, design of class and object (e.g. object layout),
> > static type analysis or inference techniques, runtime checking,
> > annotations to facilitate runtime checking, any interactions with
> > JIT/OS/GC, ... We are more interested in the design and implementation
> > issues and less so on the theoretical foundation at this point.

I have included below a summary of the responses I received.  Thanks to
all who sent information.  I have forwarded your comments to Roy.

Kathleen

*****************************************************
From: Ananda Vardhan <nandu@csa.iisc.ernet.in>
Subject: Re: object-oriented type systems in practice

Hello,

        The research going on in Secure Software Systems group in Purdue
is relevant to the mentioned issues.
        http://www.cs.purdue.edu/s3/

- -Anand        
******************************************************
From: Tiejun Wang <wtj@cs.jhu.edu>
To: kfisher@research.att.com
Cc: Scott Smith <scott@bluebird.cs.jhu.edu>
Subject: about object-oriented type systems in practice 

Hi Kathleen !

My name is Tiejun Wang. I'm a graduate student at Johns Hopkins
University, and my advisor is Scott Smith. I saw your post at The Types
Forum for information about pratical OO type systems.  

We recently have constructed a constraint-based type inference system for
Java. It has been used for static verification of Java downcasts, and can
also used as as a tool for precise concrete class analysis. There is
a paper about the system coming at ECOOP 2001. For detailed information,
please check our group's web site:
   http://www.cs.jhu.edu/labs/pll/constraints/

Best,
--Tiejun
************************************************************
From: jv@cs.purdue.edu
To: kfisher@research.att.com
Subject: oo types in practice


Dear Kathleen,

There is some work relevant to sharing from James Noble, John Potter
and David Clarke.

Furthermore, I had a paper with Boris Bokowski in Software Practice
and Experience about something called "confined types" for Java. Our
motivating example is security related.  (some version of that should
be available from my web page).

There was workshop on sharing and aliasing at ??? (I forget either
OOPSLA or ECOOP) last year with some papers on the web. 


I think that John Boyland will have a paper in the next ECOOP that
is somewhat related.



Cheers,

j


Jan Vitek                            | E-mail: jv@cs.purdue.edu
Assistant Professor                  | http://www.cs.purdue.edu/homes/jv
Dept of Computer Sciences            | Tel.  : (765) 494 6531 
Purdue University                    | Fax   :           0739
W.Lafayette, IN 47907, USA           |
*************************************************************
From: Erik Poll <erikpoll@cs.kun.nl>
To: Kathleen Fisher <kfisher@research.att.com>
Subject: Re: object-oriented type systems in practice

Hi Kathleen,

> Suggestions as to what papers would be the most relevant?  If there is
> interest, I will post a summary of the responses.

I'm not sure exactly what they are looking for - since they indicate 
quite a wide spectrum of things - but some of the things below might 
interest them.

Best regards,

Erik Poll


> > sharing objects

- A nice type system for controling sharing/aliasing, using so-called 
  "universes", is described in
  
    Peter Mueller an Arnd Poetzsch-Heffter
    Universes: A Type System for Alias and Dependency Control
    http://www.informatik.fernuni-hagen.de/import/pi5/publications.html
    
  and in 

    Peter Mueller an Arnd Poetzsch-Heffter
    Modular Specification and Verification Techniques for Object-Oriented 
    Software Components. 
    In: Foundations of Component-Based Systems, Cambridge University Press, 
        2000.

> > runtime checking, annotations to facilitate runtime checking

- Gary Leavens has a system for runtime checking of annotations in Java
  programs http://www.cs.iastate.edu/~leavens/JML.html


- The ESC group at Compaq Research Labs have developed a nice tool that 
  automatically proves annotations in Java programs. They call this 
  "extended static checking"  http://research.compaq.com/SRC/esc/