[Pl-seminar] IBM PL Day call for participation

[Mitchell Wand]

---------- Forwarded message ----------
From: Jan-Willem Maessen <Janwillem.Maessen at sun.com>
Date: Apr 30, 2007 2:19 PM
Subject: IBM PL Day call for participation
To: Jan-Willem Maessen <Janwillem.Maessen at sun.com>
Cc: Vijay Saraswat <vijay at saraswat.org>

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 to vijay @ saraswat.org (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
http://www.watson.ibm.com/general_info_haw.shtml

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 at:
http://www.watson.ibm.com/lodging.shtml

Participants are encouraged to plan a dinner with their colleagues at
neighboring restaurants. Information about local restaurants may be
found at http://www.watson.ibm.com/restaurants.shtml

AGENDA FOR IBM PL DAY (May 7, 2007)

10:00 -- 11:15 KEYNOTE M. Odersky (EPFL):
               The Scala Experience -- Safe Programming Can be Fun
11:15 -- 11:40 J.J. Hallet, V Luchangco, S Ryu, G.L. Steele (Sun):
               On coercion in programming languages
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

12:05 -- 1:30 Lunch

1:30 -- 1:55 P. Cousot, R. Cousot (Ecole Normale Superieure, Paris &
CNRS):
             Combination of abstractions in the ASTREE Static Analyzer
1:55 -- 2:20 D. Van Horn, H. Mairson (Brandeis):
             Relating complexity and precision in control flow analysis
2:20 -- 2:45 R. Grimm, L. Harris, A. Lee (NYU):
             Typical -- Taking the Tedium out of Typing
2:45 -- 3:10 S. Cherem, L. Princehouse, R. Rugina (Cornell)
             FastCheck: A practical static memory leak detection tool
for C

3:10 -- 3:40 Tea

3:40 -- 4:05 Frances Perry, L. Mackey, G. Reis, J. Ligatti, D. August,
             D. Walker (Princeton U):
             Fault-tolerant Typed Assembly Language
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
4:30 -- 4:55 G. Ghelli (U. Pisa), N. Onose (UCSD), K. Rose (IBM),
             J. Simeon (IBM):
         The Essence of Database Compilation


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

ABSTRACT

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

ABSTRACT

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

ABSTRACT

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

ABSTRACT

ASTREE [www.astree.ens.fr] 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 large
software.

=============================

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

ABSTRACT

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

ABSTRACT

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

ABSTRACT

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

ABSTRACT

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
ABSTRACT

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

ABSTRACT

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 has
lead 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.


=========================== END =============================

--
X10: Programming parallel machines, productively (http://x10.sf.net)
-------------- next part --------------
HTML attachment scrubbed and removed