June 9, 1999 Meeting

10:00am Cristian Ungureanu: A typed intermediate language for a Java native code compiler

We present a typed intermediate language used in a native code compiler for Java. The language can be used as both the source and target of various optimizations such as method dispatch elimination, and various runtime check eliminations. The IL is typed, making thus possible the detection of optimization errors through type checking.

This is join work with Suresh Jagannathan and Kim Bruce.

10:45am Chris Okasaki: Square Matrices: An Adventure in Types

Square matrices serve as an interesting case study in functional programming. Common representations, such as lists of lists, are both inefficient---at least for access to individual elements---and error-prone, because the compiler cannot enforce ``squareness''. Switching to a typical balanced-tree representation solves the first problem, but not the second. We develop a representation that solves both problems: it offers logarithmic access to each individual element and it captures the shape invariants in the type, where they can be checked by the compiler. One interesting feature of our solution is that it translates the well-known fast exponentiation algorithm to the level of types. Our implementation also provides a stress test for today's advanced type systems---it uses nested types, polymorphic recursion, higher-order kinds, and rank-2 polymorphism.

11:30am Break

11:45am Marco Antoniotti: Jester = Java || Esterel, Another Java Reactive Extension based on Esterel.

Joint work with A. Ferrari, L. Lavagno, A.L. Sangiovanni-Vincentelli.

The construction of Reactive and Embedded Systems requires sophisticated tools and firm semantics foundations to guarantee the specified performances of the final product. Moreover, the deployment of Reactive and Embedded Systems is the result of a tight interaction between software and hardware components, which get developed by a co-design process. Such process is much smoother and predictable when the supporting linguistic tools embodying the semantics foundations are easy to use and widely known. Finally, these linguistic tools should be usable as a mean to rapidly communicate design solutions between project engineers and product manufacturers.

A language system that meets the above requirements can be used as a "System Level Design Language" (SLDL).

Java is an excellent base to develop Reactive and Embedded Systems. The Embedded and Personal Java Specifications provide a reference framework for this task. Extensions to Java make the language environment even more suitable as a SLDL.

Jester extends the Java language by incorporating reactive constructs from Esterel. The reactive extensions have been carefully crafted to integrate seamlessly within the Java language framework, with two overall goal in mind: the extensions should "look familiar" to the Java programmer, and the integration of "regular" Java code in the extension should be immediately recognizable in the program text (i.e. without the use of "glue code"). Jester works as a preprocessor producing CFMS as output (in Esterel format) which can be fed into tools like POLIS or VCC (in the spirit of ECL ), or passed through the Esterel->C compilation process. The whole compilation process also fits in the Embedded Java Specification Workflow.

The system runs on any system where an Esterel compiler and a Java JDK are available. I.e. on UNI*X and WNT platforms.

Current research aims at integrating "communication" refinements in Jester. I.e. to at least provide semi automated tool to describe and implement the communication among the CFSM produced by the compilation of the synchronous units.

12:30pm Lunch

2:00pm Jonathan Moore: Chunks in PLAN: Language Support for Programs as Packets

Chunks are a programming construct in PLAN, the Packet Language for Active Networks, comprised of a code segment and a suspended function call. In PLAN, chunks provide support for encapsulation and other packet programming techniques. In this talk, I will explain the semantics and implementation of chunks. I will then proceed, using several PLAN source code examples, to demonstrate the usefulness of chunks for micro-protocols, asynchronous adaptation, and as units of authentication granularity.

2:45pm Break

3:15pm Healfdene Goguen: An Abstract Formulation of Memory Management.

We present an abstract model of computer memory, in the form of directed, labelled graphs with simple transitions corresponding to valid memory operations. We also introduce a refinement of this basic model of memory that incorporates features of memory management. After giving some examples of how this refined model captures various garbage collection algorithms, we discuss a proof that the two representations are behaviorally equivalent.

This will be an informal presentation of proofs that have been carried out in the theorem prover Coq.

The talk is an overview of work on memory management by the LEGO project at the LFCS in Edinburgh, including John Longley, Rod Burstall, Paul Jackson and me, together with Richard Brooksby and David Jones in industry.

4:00pm Talks End

Adriana Compagnoni / abc@cs.stevens-tech.edu
Last modified: Wed Aug 11 14:30:20 PDT 1999