Session 1: 10:00 - 10:45
Erik Meijer, Mircosoft
XML and Data Support Beyond XMLamda and HaskellDB
Break: 10:45 - 11:00
Session 2: 11:00 - 12:30
Phil Wadler, Avaya
Call-by-name is dual to call-by-value in the same
sense that And is dual to Or
Steve Zdancewic, University of Pennsylvania
Jif: Java + Information Flow
Lunch: 12:30 - 1:50
Business Meeting: 1:50 - 2:00
Session 3: 2:00 - 2:45
Manish Vachharajani, Princeton University
A Component Composition and Customization Language for Hardware System Simulation
Break: 2:45 - 3:00
Session 4: 3:00 - 3:45
Daniel Wang, Agere
Programming Network Processors
The early attempts resulted in a family of domain specific embedded languages in Haskell. While the DSL approach is certainly elegant, it remained a purely academic exercise. In particular it is impossible to add new syntax (for example for XML literals), and more importantly, embedding foreign type-systems into the host language requires lots of tricky type hackery (phantom types, monads, rank-n polymorphism, ...) while still not achieving full fidelity. And of course, a necessary precondition for success is that programmers buy into using a pure lazy functional language, which in practice might be the hardest problem to solve.
More recently, I have therefore been investigating how to grow the syntax and type-system of mainstream imperative object-oriented languages. This talk will discuss my current research on adding streams (lazy lists), tuples (sequences), union and intersection types, and closures plus generalized member access and joins, and XML literals to an OO language in order to gracefully unify objects, relations and trees in the real world.
Abstract: In 1990, Tim Griffen demonstrated a remarkable result: the Curry-Howard isomorphism applies to classical logic, if one extends typed lambda calculus with Scheme's call/cc operator. In 2000, Pierre-Louis Curien and Hugo Herbelin demonstrated a second remarkable result: duality in classical logic exchanges call-by-value with call-by-name. Curien and Herbelin's work was based on the lambda-mu calculus introduced by Parigot in 1992. Since lambda corresponds to implication and the dual of implication is not a common operator, this somewhat obscured the notion of duality. Here we present a new calculus based on And, Or, and Negation, which sets the duality in a more familiar context.
Abstract: Our society's widespread dependence on networked information systems for everything from personal finance to military communications makes it essential to improve the reliability and security of software. Recently, programming-languages research has demonstrated that security concerns can be addressed by using both program analysis and program rewriting as powerful and flexible enforcement mechanisms. In this talk, I will describe Jif, a variant of Java that includes mechanisms for enforcing confidentiality and integrity security policies. These security policies are expressed in an extended type system that incorporates Myers' and Liskov's decentralized label model. In addition, Jif supports robust declassification, first-class labels and principals, and label polymorphism. I will describe Jif's design, the kinds of policies expressible in the label model, and some example programs. More information about Jif is available at http://www.cs.cornell.edu/jif. The Jif project is joint work with Andrew Myers, Lantian Zheng, and Nate Nystrom, all of Cornell University.
Abstract: During hardware design, system architects use simulation extensively to validate and guide design decisions. To facilitate construction of these simulators we developed the Liberty Simulation Environment (LSE). LSE consists of a library of components, the Liberty Simulator Specification (LSS) language, and a tool that constructs a simulator based on the library and an LSS provided by the user.
In this talk, we will discuss the design considerations and tradeoffs made while developing the Liberty Simulator Specification language. The LSS language is unique in that it is designed not to specify the execution of a simulator, but rather to specify how components should be composed and customized to build a simulator. The LSS language combines several programming language techniques, including type inference and aspects, and non-standard evaluation semantics for object instantiation to ease the construction of simulators.
Abstract: Over the last few years, there has been a concerted effort to replace fixed-function ASIC chips in networking equipment by high-performance programmable "network processors". This field is still very much in its infancy, with many diverse approaches competing for survival. In this talk we will address the question "What is a network processor?". We begin by outlining application requirements for these computing devices, and then discuss how these requirements impact both processor architecture and programming models and languages. We will conclude by describing ongoing work on the design and implementation of domain specific languages for network processors.