The IBM Programming Languages Day Program Committee is pleased to invite you to participate in the 2007 IBM PL Day on May 7.

The IBM PL Day is organized in collaboration with the New England Programming Languages Symposium (NEPLS) and the New Jersey Programming Languages Symposium (NJPLS). The main goal of the event is to increase awareness of each other's work, and to encourage interaction and collaboration.

-- V. Saraswat (IBM), J.-W. Maessen (Sun), S. Zdancewic (U Penn)

REGISTRATION

If you plan to attend the Programming Languages Day, please register by sending an e-mail with your name, affiliation, and contact information (if you have not done so already). This will enable us to plan for lunch and refreshments.

LOCATION AND DRIVING DIRECTIONS

The Programming Languages day will be held at room GN-F15 in the Hawthorne1 building at 19, Skyline Drive, Hawthorne, New York 10532.

Directions to the building can be found at here.

Please follow directions at the site to visitor's entrance reception, which is on the BACK SIDE of the building. From the reception area, follow directions to room GN-F15. You will be reaching Skyline drive via Rt. 9A. Both ends of Skyline drive meet Rt. 9A. If you come in via the south end of Skyline drive, IBM Research is the first building on the right. Move to the left lane, as the right lane leads to the employee's entrance (the first entrance). Take the next entrance (the second entrance) to reception. After you go through the gate, go to the parking lot on the right side.

You are welcome from 9AM onwards, and the keynote presentation will start at 10AM sharp.

Information about local hotels can be found here. Note that the Comfort Inn in Hawthorne is located less than 2 miles from the site of the meeting.

Participants are encouraged to plan a dinner with their colleagues at neighboring restaurants. Information about local restaurants may be found at here.

AGENDA FOR IBM PL DAY (May 7, 2007)

Abstract for talks

10:00 -- 11:15 KEYNOTE M. Odersky (EPFL): The Scala Experience -- Safe Programming can be fun

Scala is a new general purpose programming language which is fully inter-operable with Java. It smoothly integrates features of object-oriented and functional languages. Scala allows a terseness of style comparable to scripting languages but has at the same time a strong and static type system. In this way, it can express common programming patterns in a concise, elegant, and type-safe way.

This talk will give an introduction to the Scala programming language, highlighting its main innovative features: closures, pattern matching, type abstraction, and mixins. I will show how these features together enable the construction of truly high-level libraries that provide in effect embedded domain-specific languages. I will also give an outline how Scala's higher-level constructs are mapped to Java.

11:15 -- 11:40 J.J. Hallet, V Luchangco, S Ryu, G.L. Steele (Sun): On coercion in programming languages

Coercion (i.e., implicit type conversion) can greatly improve the readability of programs, especially in arithmetic expressions. However, coercion interacts with other features of programming languages, particularly subtyping and overloaded functions and operators, in ways that can produce surprising behavior. We examine coercion as provided in several languages--from Fortran, which coerces only between predefined numeric types in arithmetic expressions, to C\#, which supports user-defined coercion that may be combined with subtyping and predefined coercion and applied in almost any expression context--to learn how to support coercion in a way that minimizes confusion while still reaping its main benefits. We apply these lessons to our design of the coercion mechanism in Fortress, a language with support for overloading with multiple dynamic dispatch, multiple inheritance, and user-defined coercion. We show how our restrictions on overloaded declarations prevent ambiguous calls due to coercion. We also show how coercion in Fortress supports ``widest-need evaluation'' in numeric computations, which ensures that precision is not lost in the computation of intermediate subexpressions of a compound expression.

11:40 -- 12:05 M.-C. Marinescu, J. Field (IBM), C. Stefansen (U. Copenhagen) Reactors: A Data-oriented synchronous/asynchronou sprogramming model for distributed applications

In modern web applications, the traditional boundaries between browser-side presentation logic, server-side ``business'' logic, and logic for persistent data access and query are rapidly blurring. This is particularly true for so-called web mash-ups, which bring a variety of data sources and presentation components together in a browser, often using asynchronous (``AJAX'') logic. Such applications must currently be programmed using an agglomeration of data access languages, server-side programming models, and client-side scripting models; as a consequence, programs have to be entirely rewritten or significantly updated to be shifted between tiers.

In this talk, we define the kernel of a simple and uniform programming model---the _reactor_ model---suitable for building and evolving internet-scale programs. Our goal is to use the reactor model as the foundation for the design of a uniform programming language for web applications, other human-driven distributed applications, and distributed business processes or web services which can express application logic, user interaction, and business logic using the same basic programming constructs.

A reactor consists of two principal components: mutable state, in the form of a fixed collection of _relations_, and code, in the form of a fixed collection of _rules_ in the style of datalog. A reactor's code is executed in response to an external \emph{stimulus}, which takes the form of an attempted update to the reactor's state.

As in classical process calculi, the reactor model accommodates collections of distributed, concurrently executing processes. However, unlike classical process calculi, our observable behaviors are sequences of states, rather than sequences of messages. Similarly, the interface to a reactor is simply its state, rather than a collection of message channels, ports, or methods.

One novel feature of our model is the ability to compose behaviors both synchronously and asynchronously. Also, our use of datalog-style rule allows aspect-like composition of separately-specified functional concerns in a natural way, thus simplifying composition, evolution, and maintenance of distributed applications.

1:30 -- 1:55 P. Cousot, R. Cousot (Ecole Normale superieure, Paris & CNRS) Combination of abstractions in the ASTREE Static Analyzer

ASTREE is an automatic static analyzer for proving the absence of runtime errors in programs written in C ASTREE's design is formally founded on the theory of abstract interpretation. ASTREE is designed to be highly capable and extremely competitive on safety- critical real-time synchronous control-command programs. On this family of programs, ASTREE produces very few false alarms (i.e. signals of potential runtime errors that are due to the imprecision of the static analysis but can never happen at runtime in any actual execution environment). ASTREE can be tuned to get no false alarms thanks to parameters and directives, which inclusion can be automatized. In absence of any alarm, ASTREE's static analysis provides a proof of absence of runtime errors.

We describe the structure of the abstract domains in the ASTREE static analyzer, their modular organization into a hierarchical network, their cooperation to over-approximate the conjunction/reduced product of different abstractions and to ensure termination using collaborative widenings and narrowings. This separation of the abstraction into a combination of cooperative abstract domains makes ASTREE extensible, an essential feature to cope with false alarms and ultimately provide sound formal verification of the absence of runtime errors in very largesoftware.

1:55 -- 2:20 D. Van Horn, H. Mairson (Brandeis): Relating complexity and precision in control flow analysis

We analyze the computational complexity of kCFA, a hierarchy of control flow analyses that determine which functions may be applied at a given call-site. This hierarchy specifies related decision problems, quite apart from any algorithms that may implement their solutions. We identify a simple decision problem answered by this analysis and prove that in the 0CFA case, the problem is complete for polynomial time. The proof is based on a nonstandard, symmetric implementation of Boolean logic within multiplicative linear logic (MLL). We also identify a simpler version of 0CFA related to eta-expansion, and prove that it is complete for LOGSPACE, using arguments based on computing paths and permutations.

For any fixed k>0, it is known that kCFA (and the analogous decision problem) can be computed in time exponential in the program size. For k=1, we show that the decision problem is NP-hard, and sketch why this remains true for larger fixed values of k. The proof technique depends on using the approximation of CFA as an essentially nondeterministic computing mechanism, as distinct from the exactness of normalization. When k=n, so that the ``depth'' of the control flow analysis grows linearly in the program length, we show that the decision problem is complete for EXPTIME.

In addition, we sketch how the analysis presented here may be extended naturally to languages with control operators. All of the insights presented give clear examples of how straightforward observations about linearity, and linear logic, may in turn be used to give a greater understanding of functional programming and program analysis.

2:20 -- 2:45 R. Grimm, L. Harris, A. Lee (NYU) Typical -- Taking the Tedium Out of Typing

Language designers and compiler developers rely on domain-specific languages and the corresponding compiler-compiler tools to generate a compiler's parser, optimization, and code generation phases. Unfortunately, little comparable support is available for creating the semantic analysis phase---even though type checkers are critical for program safety and require a non-trivial engineering effort. Based on the observation that typing rules, whether specified in prose or in formal notation, are highly structured, this talk presents Typical, a domain-specific language and compiler to make type checkers for real-world languages easier to implement and extend. Our language builds on existing functional programming techniques to provide a well-defined semantics and extends them with declarative constructs where appropriate. Notably, Typical incorporates the functional core of ML, since variant types and pattern matching enable a direct and elegant expression of a type system's case analysis. It also provides a system-wide ``no information'' monad to simplify error management, including to avoid cascading error messages. On top of this functional core, Typical provides declarative constructs for expressing scoping rules, namespaces, and constraints on types and their attributes. Finally, its module system relies on rule rewriting to provide extensibility, supporting the introduction of new types, attributes, and constraints. While our language is largely functional, the rest of the compiler need not be. In fact, our Typical compiler generates Java and the resulting type checkers seamlessly integrate with other imperative code. Our experimental comparison of Typical and C type checkers written in Typical and Java demonstrates that our system is effective, supporting the concise specification of real-world type checkers that also exhibit competitive performance.

2:45 -- 3:10 S. Cherem, L. Princehouse, R. Rugina (Cornell) FastCheck: A practical static memory leak detection tool for C

I will present FastCheck, a static analysis tool for detecting memory leaks in C programs. FastCheck tracks the flow of values from allocation points to deallocation points using a sparse representation of the program. Our sparse representation consists of a guarded value-flow graph. The graph captures def-use relations and value flows via program assignments. Edges in the graph are annotated with guards that describe branch conditions in the program. The value-flow represented by an edge can occur when the branches indicated by the edge's guard are taken.

The memory leak analysis is reduced to a reachability problem over the guarded value-flow graph. Given an allocation, we first find if the allocated value flows to any free statement. If so, we use the guards to reason about the branches that must be taken for a deallocation to happen. With the aid of a SAT solver, FastCheck can determine when a combination of branch decisions leads to no deallocation and produces a memory leak. The sparse program representation allows FastCheck to focus on the portions of the program relevant to the leak problem. This makes FastCheck efficient in practice, and allows it to report concise error messages. We have run FastCheck on the SPEC 2000 benchmarks and on two open-source applications, bash and sshd, and found around 60 memory leaks. FastCheck prioritizes the warnings it generates and achieves a false positive rate below 20% for these programs.

3:40 -- 4:05 Frances Perry, L. Mackey, G. Reis, J. Ligatti, D. August, D. Walker (Princeton U): Fault-tolerant Typed Assembly Language

A transient hardware fault occurs when an energetic particle strikes a transistor, causing it to change state. Although transient faults do not permanently damage the hardware, they may corrupt computations by altering stored values and signal transfers. In this talk, we propose a new scheme for provably safe and reliable computing in the presence of transient hardware faults. In our scheme, software computations are replicated to provide redundancy while special instructions compare the results of replicas to detect errors before writing critical data. In stark contrast to any previous efforts in this area, we have analyzed our fault tolerance scheme from a formal, theoretical perspective. In addition to the formal analysis, we evaluate the execution time of our detection scheme to quantify the performance penalty for sound fault tolerance.

4:05 -- 4:30 M. Pistoia (IBM), A. Banerjee (Kansas State), D. A. Naumann (Stevens Institute of Technology): Beyond Stack Inspection: A Unified Access-Control and Information-Flow Security Model

Modern component-based systems, such as Java and Microsoft .NET Common Language Runtime (CLR), have adopted Stack-Based Access Control (SBAC). Its purpose is to use stack inspection to verify that all the code responsible for a security-sensitive action is sufficiently authorized to perform that action. However, previous literature has shown that the security model enforced by SBAC is flawed in that stack inspection may allow unauthorized code no longer on the stack to influence the execution of security-sensitive code. A different approach, History-Based Access Control (HBAC), is safe but may unjustly prevent authorized code from executing a security-sensitive operation if less trusted code was previously executed. In this paper, we formally introduce Information-Based Access Control (IBAC), a novel security model that verifies that all and only the code responsible for a security-sensitive operation is sufficiently authorized. Given an access-control policy, we present a mechanism to extract from it an implicit information-flow policy, and we prove that IBAC enforces both policies. Furthermore, we discuss large-scale application code scenarios to which IBAC can be successfully applied.

4:30 -- 4:55 G. Ghelli (U. Pisa), N. Onose (UCSD), K. Rose (IBM), J. Simeon (IBM): The Essence of Database Compilation

The extension of XQuery with side-effects is being investigated by the W3C, and is the focus of several research projects. The Holy Grail of these projects is the ability to support side-effect operations similar to those of programming languages, while preserving known optimization techniques used for pure query languages. Our quest haslead us to reexamine the foundations of query language semantics and compilation. In this paper, we propose a functional semantic for XQuery based on comprehensions as an alternative to the one proposed by W3C. The main benefit of this approach is to precisely correspond with compilation into a typed algebra that supports traditional database optimizations. It also provides insights into the nature of database compilers. We notably discover that type systems for database algebras require an original solution to the old problem of subtyping with record concatenation, and that such a type system can eliminate the need for complex side conditions used in database optimization. Finally, it is such that the standard state monad approach can be used to handle side-effects both at the semantic and algebraic levels.