We gather from 12.45. Talks start at 1.00 and should be finished by 1.50 at the latest, thereby allowing time for some questions and people to get to other meetings by 2.00. Shorter talks are fine too. There's a data projector and whiteboard in the room; if you need an OHP please let me know in advance.
The Logic and Semantics seminar has more formal talks, with introductions and applause (both of which get omitted in SL), usually on Fridays at 2pm. It is coordinated by Tom Ridge.
Peter.Sewell@cl.cam.ac.uk
Program errors are hard to detect and are costly both to programmers who spend significant efforts in debugging, and for systems that are guarded by runtime checks. Static verification techniques have been applied to imperative and object-oriented languages, like Java and C\#, but few have been applied to a higher-order lazy functional language, like Haskell. In this paper, we describe a sound and automatic static verification tool for Haskell, that is based on contracts and symbolic execution. Our approach is modular and gives precise blame assignments at compile-time in the presence of higher-order functions and laziness. (This paper is accepted by POPL'09.)
The category of nominal sets provides a mathematical model of names and binding based on simple, but subtle ideas to do with permutations of names and "finitely supported" mathematical objects that first arose in mathematical logic in the 1930s. Its use underlies a number of recent works on names and binding in computational logic, automated reasoning, programming language design and operational semantics. Relatively little use has been made of it for denotational semantics. Yet the key notion of finite support provides a syntax-independent model of "free occurrence of names" that really comes into its own when considering the kind of infinite mathematical objects that arise in semantics rather than syntax. So this talk will explain what is known so far about "doing domain theory in the category of nominal sets", in the hope that some of the audience will be attracted to do some more.
From the point of view of the semanticist, one of the chief attractions of functional programming is the close connection of the typed lambda calculus to proof theory and logic via the Curry-Howard correspondence. The point of view of the workaday programmer seems, at first glance, less exalted - one of the most compelling features in actual programming languages like ML and Haskell is the ability to analyze structured data with pattern matching. But pattern matching, though enormously useful, has historically lacked the close tie to logic that the other core features of functional languages possess.
The Definition of Standard ML, for example, contains a suggestion in English that it would be desirable to check coverage, with no clear account of what this means or how to accomplish it. In this talk we will argue the semanticist ought to be just as interested in pattern matching as the programmer. We show that pattern matching has a strong logical interpretation via the proof-theoretic notion of focusing, and that filling in this part of the Curry-Howard correspondence enables simple correctness proofs of parts of the compiler (such as the coverage checker and the pattern compiler) that required considerable insight and creativity before.
(This work will appear in POPL 2009.)
Rely-guarantee is a well-established approach to reasoning about concurrent programs that use parallel composition. However, parallel composition is not how concurrency is structured in real systems. Instead, threads are started by `fork' and collected with `join' commands. This style of concurrency cannot be reasoned about using rely-guarantee, as the life-time of a thread can be scoped dynamically. With parallel composition the scope is static.
In this talk, we will describe deny-guarantee reasoning, a reformulation of rely-guarantee that enables reasoning about dynamically scoped concurrency. Deny-guarantee builds on ideas from separation logic to allow interference to be dynamically split and recombined, in a similar way that separation logic splits and joins heaps. To allow this splitting, the rely is inverted to give a deny, specifying what the environment cannot do. We illustrate the use of our proof system with examples, and show that it can encode all the original rely-guarantee proofs.
Abstract: In this talk I will describe various notions of syntactic logical relations for pure System F without recursion. I will then attempt to connect these relations to various notions of bisimulation and observational equivalence. It turns out that even in this simple setting the connection of these logical relations to observational equivalence is not obvious; and I will be explaining the complications and some ideas to solve this problem. There are few novel results in this talk so this is mainly a call for discussion on ways forward.
We describe a semantic type soundness result, formalized in the Coq proof assistant, for a compiler from a simple functional language into an idealized assembly language. Types in the high-level language are interpreted as binary relations, built using both second-order quantification and separation, over stores and values in the low-level machine.
This is joint work with Nicolas Tabareau from PPS, Paris 7.
It is well-known that finding shortest paths in a graph corresponds to solving a matrix equation, and that this can be done by an iterative process. This is guaranteed to converge to a fixed point if the underlying algebra of the matrix elements has certain properties.
We will look at the related notion of a "stable paths problem", where the solution that is sought is not an optimal shortest-paths tree, but a Nash equilibrium of path assignments. The same matrix methods can be used to solve this problem, but the algebraic properties involved are different.
This talk will concentrate on proofs of convergence for the matrix iteration, and the associated problem of how many iteration steps may be required before a fixed point is reached.
The unfolding of (1-)safe Petri nets to occurrence nets is well understood. There is a universal characterization of the unfolding of a safe net which is part and parcel of a coreflection from the category of occurrence nets to the category of safe nets. The unfolding of general Petri nets, nets with multiplicities on arcs whose markings are multisets of places, does not possess a directly analogous universal characterization, essentially because there is an implicit symmetry in the multiplicities of general nets, and that symmetry is not expressed in their traditional occurrence net unfoldings. In our paper, we show how to recover a universal characterization by representing the symmetry in the behaviour of the occurrence net unfoldings of general Petri nets. We show that this is part of a coreflection between enriched categories of general Petri nets with symmetry and occurrence nets with symmetry.
(A preview of an FSTTCS talk, joint work with Glynn)
Storing state in the client tier (in forms or cookies, for example) improves the efficiency of a web application, but it also renders the secrecy and integrity of stored data vulnerable to untrustworthy clients. We study this general problem in the context of the Links multi-tier programming language.
We eliminate these threats by augmenting the Links compiler to encrypt and authenticate any data stored on the client. We model this compilation strategy as a translation from a core fragment of the language to a concurrent lambda-calculus equipped with a formal representation of cryptography. To formalize source-level reasoning about Links programs, we define a type-and-effect system for our core language; our implementation can machine-check various integrity properties of the source code. By appeal to a recent system of refinement types for secure implementations, we show that our compilation strategy guarantees all the properties provable by our type-and-effect system.
Inheritance is a standard means for reuse and for interfacing with external libraries. In a multi-language software product, extending a class written in a statically-typed language with a dynamically-typed class can require a significant number of manual indirections and other error-prone complications. Building on our previous interoperability work, we introduce a technique that allows safe, easy inheritance across languages. We demonstrate our technique for cross- language inheritance with a statically-typed object calculus and a dynamically-typed object calculus, where a statically-typed class can extend a dynamically-typed one and vice versa. We provide a proof sketch of soundness, as well as a guarantee that dynamic type errors do not arise due to statically-typed expressions.
ABSTRACT: I will present CMod, a novel tool that provides a sound module system for C. CMod works by enforcing a set of four rules that are based on principles of modular reasoning and on current programming practice. CMod's rules flesh out the convention that .h header files are module interfaces and .c source files are module implementations. Although this convention is well-known, existing explanations of it are incomplete, omitting important subtleties needed for soundness. In contrast, we have proven formally that CMod's rules enforce both information hiding and type-safe linking.
To use CMod, the programmer develops and builds their software as usual, redirecting the compiler and linker to CMod's wrappers. We evaluated CMod by applying it to 30 open source programs, totaling more than one million lines of code. Violations to CMod's rules revealed more than a thousand information hiding errors, dozens of typing errors, and hundreds of cases that, although not currently bugs, make programming mistakes more likely as the code evolves. At the same time, programs generally adhere to the assumptions underlying CMod's rules, and so we could fix rule violations with a modest effort. We conclude that CMod can effectively support modular programming in C: it soundly enforces type-safe linking and information hiding while being largely compatible with existing practice.
For more information, see here.