*Abstract:* Two successful ways of describing the denotational
semantics of programming languages may be distinguished: the
*extensional* approach taken by domain theory, and an
*intensional* one, exemplified by game semantics. Our goal is to
combine the advantages of both by drawing the two traditions
together--to describe an extensional semantics of program behaviour
based on the order-theoretic characterisation of sequential
higher-order functions. The latter has been a long-standing area of
study in denotational semantics, but its ramifications go beyond purely
functional computation. As the development of game semantics shows,
insights into sequential behaviour may be employed in modelling a
range of computational effects such as locally bound references.

In this talk, I will describe a notion of sequential function based
on *bistability*. This exploits the duality between two kinds
of failure--divergence (bottom) and error (top)--to obtain a complete
order-theoretic description of the behaviour of functional
programs. It can be neatly expressed using a partial order with an
involutive "negation" operation which exchanges bottom and top.

A key property characterising such *locally boolean* domains
is that they can be constructed using three operations--indexed
products and separated sums, and limits of omega-chains. This exposes
a natural connection with game semantics: a domain in "prenex normal
form" Pi_{i in I} Sigma_{j in Ji}
A_{ij} corresponds to a two-player game in which one player
chooses indices in the product, and the other chooses indices in the
sum. Moreover, the bistable functions correspond to *strategies*
for these games.

Using these properties we can construct a model of linear logic from locally boolean domains. This has some interesting additional "sequential" connectives which we can use to derive a semantics of functional computation with local state.

*Abstract:* The goal of the SLAM project is to analyze system
software written in C, and check it against temporal safety
properties. The SLAM toolkit uses model checking, program analysis and
theorem proving techniques to do automatic analysis, and requires no
user-supplied abstractions or annotations such as pre-conditions,
post-conditions or loop invariants. We have successfully applied the
SLAM toolkit to over 100 Windows device drivers, to both validate
their behavior and find defects in their usage of kernel-level
APIs. The SLAM toolkit currently is in transition from a research
prototype to a product-grade tool that will be supported and used by
the Windows development organization.

I will start by describing the ideas and algorithms behind SLAM. As is often the case, there is a gap between the theory and algorithms one publishes and the implementation of a tool that has been engineered to perform acceptably in practice. In the second half of the talk, I will detail some of the engineering "secrets" we applied to the basic SLAM process to improve its performance on Windows device drivers. (Joint work with Thomas Ball, Microsoft Research.)

*Abstract:* The rules of classical logic may be formulated in
pairs corresponding to De Morgan duals: rules about "and" are dual to
rules about "or". A line of work, including that of Filinski (1989),
Griffin (1990), Parigot (1992), Danos, Joinet, and Schellinx (1995),
Selinger (1998,2001), and Curien and Herbelin (2000), has led to the
startling conclusion that call-by-value is the de Morgan dual of
call-by-name.

This paper presents a dual calculus that corresponds to the classical sequent calculus of Gentzen (1935) in the same way that the lambda calculus of Church (1932,1940) corresponds to the intuitionistic natural deduction of Gentzen (1935). The paper includes crisp formulations of call-by-value and call-by-name that are obviously dual; no similar formulations appear in the literature. The paper gives a CPS translation and its inverse, and shows that the translation is both sound and complete, strengthening a result in Curien and Herbelin (2000).

Organizers, appsem04(at)cs.ioc.ee

Last update 7 May 2004