Session 1: 10:00 - 11:30
Philip Wadler, Avaya Labs
Call-by-name is dual to call-by-value
Andrew Myers, Cornell University
Iterable Pattern Matching for Java
Break: 11:30 - 11:45
Session 2: 11:45 - 12:30
Daniel Wang, Agere
Programming Network Processors
Lunch: 12:30 - 1:50
Business Meeting: 1:50 - 2:00
Session 3: 2:00 - 2:45
Robert Muller (Boston College)
Inferring Annotated Types for Inter-procedural Register Allocation
with Constructor Flattening
Break: 2:45 - 3:00
Session 4: 3:00 - 3:45
Manish Vachharajani (Princeton University)
A Component Composition and Customization Language for
Hardware System Simulation
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:The JMatch language extends Java with _abstract iterable pattern matching_, pattern matching that is compatible with the data abstraction features of Java and makes iteration abstractions convenient. JMatch has ML-style deep pattern matching, but patterns can be abstract; they are not tied to algebraic data constructors. A single JMatch method may be used in several modes; modes may share a single implementation as a boolean formula. Modal abstraction simplifies specification and implementation of abstract data types. This talk will describe the JMatch language and its implementation. Joint work with Jed Liu.
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.
Abstract: We introduce an annotated type system for a compiler intermediate language. The type system is designed to support inter-procedural register allocation and the representation of tuples and variants directly in the register file. We present an algorithm for assigning annotations and prove its soundness with respect to the type system.
Joint work with Torben Amtoft, Kansas State 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.