Arrival and Coffee: 9:30 - 10:00
Session 1: 10:00 - 12:15
David Sands (Chalmers University of Technology, Sweden)
Controlled Downgrading based on Intransitive (Non)Interference
Adriana Compagnoni (Stevens Institute of Technology)
Correspondence assertions for process
synchronization in concurrent communications
Mukund Raghavachari (IBM T.J. Watson Research Center)
XJ: The Integration of XML and Java
Lunch: 12:30 - 1:55
Business meeting: 1:55 - 2:00
Session 2: 2:00 - 3:30
Andrew W. Appel (Princeton University)
Foundational Proof-Carrying Code version 2003
Rahul Agarwal (SUNY Stony Brook)
Type Inference for Parameterized Race-Free Java
Joint work with Heiko Mantel, ETH Zurich
Abstract: High-level specification of patterns of communications such as protocols can be modeled elegantly by means of session types. However, a number of examples suggest that session types fall short when finer precision on protocol specification is required. In order to increase the expressiveness of session types, we appeal to the theory of correspondence assertions. The resulting type discipline augments the types of long term channels with effects and thus yields types which may depend on messages read/written earlier within the same session. We prove that evaluation preserves typability and that well-typed processes are safe. Also, we illustrate how the resulting theory allows us to address the shortcomings present in the pure theory of session types.
This is joint work with Eduardo Bonelli and Elsa Gunter.
Abstract: The importance of XML in data integration has led to several efforts to simplify the development of programs that operate on XML data. A common goal of these efforts is to provide higher-level support for XML in programming languages. The subject of this paper is XJ, a research language that integrates XML as a first-class construct into Java. The design goals of XJ distinguish it from other projects that integrate XML into programming languages --- specifically, XJ supports in-place updates of XML data, thus making the composed language truly imperative, and it adheres to XML standards such as XML Schema and XPath.
Abstract: Can one formally prove useful properties of real programs? And if so, would it be worth the trouble?
These questions have been asked for 40 years. By 1980, the answers were fairly clearly established: No, and No.
In the last two decades that there has been enough progress in programming-language design, programming-language semantics, and automated theorem proving, to produce at least one domain in which the answers are Yes, and Yes.
The Foundational Proof-Carrying Code project at Princeton is an attempt to specify, prove, and check safety properties of machine-language programs, in a scalable way that can be useful in the real world. I'll explain our approach.
Abstract: We study the type system introduced by Boyapati and Rinard in their paper ``A Parameterized Type System for Race-Free Java Programs'' and try to infer the extra annotations, i.e., the lock types needed by the PRFJ typechecker to determine if the program is race free or not. Boyapati and Rinard use default types and infer local variable owners to automatically annotate some of the lock types, but in practice, the programmer still needs to annotate on the order of 1 in every 25 lines of code. We try to do a more exhaustive annotation of the code. Static inference of annotations requires an expensive points-to and locks-held analysis, so we use runtime techniques, based on the lockset algorithm, in conjunction with some static analysis to infer the lock types.
This is joint work with Scott Stoller.