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" Pii in I Sigmaj in Ji Aij 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).