Anindya Banerjee, Department of Computing and Information Sciences, Kansas State University

Prakash Panangaden, School of Computer Science, McGill University

The fact that lambda-calculus can be encoded in first order concurrent languages was discovered by Milner - in the context of the pi-calculus - and thoroughly explored by Sangiorgi and several others. A few years earlier linear logic was invented by Girard and led to an explosion of interest in the relation between proof theory and computation. Abramsky developed Linear Realizability Algebra as a computational formalism related to linear logic in the same was that simply typed lambda-calculus relates to intuitionistic propositional logic. In this talk I show that the encoding of lambda-calculus into pi-calculus and other similar formalisms (like concurrent constraint programming) can be mediated through the translation of lambda-calculus into Linear Realizability Algebra. As far as I know the translation of lambda-calculus into Linear Realizability Algebra is new.

This is joint work with Samson Abramsky and Radha Jagadeesan.

Benoît Valiron, Department of Mathematics and Statistics, University of Ottawa

The objective of this paper is to develop a functional programming language for quantum computers. We develop a lambda calculus for the classical control model, following Peter Selinger's work on quantum flow-charts. We define a call-by-value operational semantics, and we give a type system using affine intuitionistic linear logic. The main results of this paper are the safety properties of the language and the development of a type inference algorithm.

This is joint work with Peter Selinger

Dominique Boucher, NuEcho Inc.

We present a domain-specific language (DSL) for the specification of dialog components. The language is based on hierarchical state machines. It features many concepts normally found in modern programming languages: (single) inheritance, lexical scoping, a module system. An overriding mechanism also helps customizing internal states in a declarative way.

We show how this language helps in codifying "dialog best practices" and "dialog patterns" across an entire application.

Christopher J.F. Pickett, McGill University

Speculative multithreading (SpMT) is a technique for automatic parallelisation of single-threaded programs. Speculative Method-Level Parallelism (SMLP), a variant of SpMT, performs significantly better in the presence of accurate return value prediction.

We present the design and implementation of return value prediction in SableVM, a Java Virtual Machine, and include existing finite context method (FCM) and hybrid predictors from the literature. We also describe and characterize a new table-based memoization predictor that complements these predictors nicely.

We then look to improving return value prediction further using Soot, our Java bytecode compiler framework. We present an interprocedural parameter dependence analysis that eliminates parameter inputs to our memoization predictor that do not affect the return value. We also present a return value use analysis to determine which return values are consumed, and furthermore label those that are only used inside boolean and branch expressions. The results of these analyses are encoded in attributes and exploited by the VM at runtime.

This is joint work with Clark Verbrugge

Stefan Monnier |