Abstracts

Tutorial Lectures

Andrew Appel. The Turing machine in the voting booth

Abstract. Citizens of democracies vote using procedures and technologies that have changed over the past 250 years. In response to abuse and manipulation of one procedure or technology, a new one is introduced. In the 19th century, the preprinted secret ballot was introduced to combat voter intimidation; in the early 20th century, mechanical lever-action machines combated paper-ballot fraud.

In the mid-20th century, Turing and von Neumann outlined the general-purpose stored-program computer, capable of performing or simulating any computation, and within a few decades computers were used to count votes. We would like to know that the votes are counted accurately, even though there are substantial incentives to cheat. We can apply basic principles of computation and of computer security to see why this problem is so difficult; we can compare with solved problems (bank ATM machines) and unsolved problems (digital rights management).

Jesper Bengtson, Uppsala University, Karthikeyan Bhargavan, Cédric Fournet and

Andrew D. Gordon, Microsoft Research, Sergio Maffeis, Imperial College London and University of California at Santa Cruz. Refinement Types for Secure Implementations

Abstract. We present the design and implementation of a typechecker for verifying security properties on the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a lambda-calculus equipped with refinement types for expressing pre- and post-conditions within first-order logic. We derive formal cryptographic primitives and represent active adversaries within the type theory. Well-typed programs enjoy assertion-based security properties, with respect to a realistic threat model including key compromise. The implementation amounts to an enhanced typechecker for the general purpose functional language F#; typechecking generates verification conditions that are passed to an SMT solver. We describe a series of checked examples. This is the first tool to verify authentication properties of cryptographic protocols by typechecking their source code.

The paper accompanying this talk will appear in the proceedings of the 2008 IEEE Computer Security Foundations Symposium.

Luca Cardelli. On process rate semantics

Abstract. We provide translations between process algebra and systems of chemical reactions. We show that the translations preserve discrete-state (stochastic) and continuous-state (concentration) semantics, and in particular that the continuous-state semantics of processes corresponds to the differential equations of chemistry based on the law of mass action. The novel semantics of processes so obtained equates processes that have the same state occupation dynamics, but that may have different interaction interfaces.

Konstantinos Chatzikokolakis and Keye Martin. A monotonicity principle for information theory

Abstract. We establish a monotonicity principle for convex functions that enables high-level reasoning about capacity in information theory. Despite its simplicity, this single idea is remarkably applicable. It leads to a significant extension of algebraic information theory, a solution of the capacity reduction problem, intuitive graphical methods for comparing channels, new inequalities that provide useful estimates on the information transmitting capability of a channel operating in an unknown environment, further explication of the fascinating relationship between capacity and Euclidean distance, and the solution of an open problem in quantum steganography

Bob Coecke, Eric Oliver Paquette and Simon Perdrix. Bases in diagrammatic quantum protocols

Abstract. Categorical axiomatisation of quantum mechanics enables rigourous and abstract design of quantum protocols. This program was initiated by Abramsky and Coecke in their analysis of the quantum teleportation protocol. They showed that dagger compact categories capture essential structures of the quantum mechanical formalism for diagrammatic design of teleportation.

In this paper, we show that the use of base structures, i.e. an axiomatisation of orthonormal bases of Hilbert space within a dagger symmetric monoidal category, leads to a diagrammatic description, among other protocols, of Perdrix' state transfer protocol. State transfer is key to the unification of measurement-only and one-way models of quantum computation. Moreover, state transfer, as a substitute for teleportation, is a key feature for optimizing the resources of measurement-only quantum computation. The diagrammatic analysis of both teleportation and state transfer reveals structural connections between these two measurement-only quantum computational models.

Our notion of basis structure refines the classical objects of Coecke and Pavlovic in an essential manner: it bypasses the conflict between: i.~the necessarily `self-dual' dagger Frobenius comonoids, and, ii.~the compact structures with `non-trivial duals' required to accommodate Selinger's diagrammatic representation of mixed states and operations. One interpretation of our basis structures is that they do not refine, but are complementary to compactness of a dagger symmetric monoidal category. A complementary view is that they do not only refine the compact structures in terms of a comonoid structure, but also require an `un-natural' explicit witness for the passage from a space to its dual, hence reconciling the `natural' compact structures with the `un-natural' dagger Frobenius comonoids.

This refinement also allows us to both accommodate physical flow of information and logical flow of information within one language, hence enriching the currently used diagrammatic languages with an important new feature.

Yannick Delbecque and Prakash Panangaden. Game semantics for quantum stores.

Abstract. This paper presents a game semantics for a simply typed $\lambda$-calculus equipped with quantum stores. The quantum stores are equipped with quantum operations as commands. This gives the language enough expressiveness to encode any quantum circuits. The language uses a new construct: compound variables which one can think of as a ``tensor of variables'' to refer to quantum stores. This allows one to keep track of the size of the states which the store contains. The game semantics is constructed from classical game semantics using interventions operators to encode the effects of the operations commands. A soundness result for the semantics is given.

Robert Dockins, Andrew Appel and Aquinas Hobor. Multimodal separation logic for reasoning about operational semantics

Abstract. We show how to reason, in the proof assistant Coq, about realistic programming languages using a combination of separation logic and heterogeneous multimodal logic. A heterogeneous multimodal logic is a logic with several modal operators that are not required to satisfy the same frame conditions. The result is a powerful and elegant system for reasoning about programming languages and their semantics. The techniques are quite general and can be adopted to a wide variety of settings.

Derek Dreyer. Good Fibrations: Simplifying and generalizing the ML module system.

Abstract. The ML module system provides powerful support for namespace management, data abstraction, and code reuse, and has proven effective in practice. Furthermore, it has served as a good basis for language evolution: a number of extensions and improvements to the language (translucent signatures, higher-order functors, first-class modules) have been proposed and implemented without requiring any changes to the basic structure of the module system.

However, we observe two seemingly unrelated problems. First, attempts over the past decade to extend ML with recursive module definitions have failed to provide general support for separate compilation, which is one of the key purposes of a module system. Second, there exists a common perception among many language researchers that, while the ML module system is very powerful, it has (to quote Peyton Jones) a "poor power/cost ratio" in terms of language complexity.

We argue that both of these problems are to a great extent attributable to a schizophrenic divergence between the way that the ML module system encodes signature families vs. module families. Signature families are defined by what Harper and Pierce have dubbed

"fibration" (the category-theoretic reference being merely "analogical"), whereas module families are defined by "parameterization" (i.e. functors).

Harper and Pierce argue persuasively that fibration is superior to parameterization for signatures, and we argue that fibration is a good idea for modules as well. Fortunately, this idea has already been proposed and studied in depth (by Bracha, Ancona and Zucca, et al.) under the name "mixin modules." Unfortunately, mixin modules traditionally lack support for type components, and previous attempts to add type components to mixins have not resulted in language designs that properly subsume the ML module system.

We describe a novel foundational module calculus called MixML that supports very simple encodings of all the major features of the ML module system, as well as several extensions, such as separate compilation of recursive modules. Despite being more powerful than ML, it is in fact simpler, with a minimalist syntax and a very small set of orthogonal constructs. The key idea is to unify the structure and signature languages of ML into one language of MixML modules. This permits a uniform representation of structure and signature composition via hierarchical mixin composition (i.e. fibration), from which the alternative "parameterization" approach to module and signature families falls out as a stylized mode of use.

We also discuss the key type-theoretic challenges that we had to overcome in order to work out the type system for MixML. The primary challenge was the "double vision problem," a rather basic problem involving the interaction of recursion and abstract data types that to our knowledge has received scant attention in the type theory and semantics literature.

This is joint work with Andreas Rossberg.

Peter Dybjer. The interpretation of intuitionistic type theory in locally cartesian closed categories: an intuitionistic approach

Abstract. I will give an intuitionistic view of Seely's interpretation of Martin-Löf type in locally cartesian closed categories. The point is to use Martin-Löf type theory itself as metalanguage, and a constructive notion of category, a so called E-category. As a categorical substitute for the formal system of Martin-Löf type theory I will use E-categories with families, and discuss how to interpret such categories in E-locally cartesian closed categories. This is joint work with Alexandre Buisse, who has formalized the key part of this proof in Coq.

Marcelo Fiore and Chung-Kil Hur. Term equational systems and logics

Abstract. We introduce an abstract general notion of system of equations between terms, called Term Equational System, and develop a sound logical deduction system, called Term Equational Logic, for equational reasoning. Further, we give an analysis of algebraic free constructions that together with an internal completeness result may be used to synthesize complete equational logics. Indeed, as an application, we synthesize a sound and complete nominal equational logic, called Synthetic Nominal Equational Logic, based on the category of Nominal Sets.

Joshua D. Guttman. Fair exchange in strand spaces

Abstract. A cryptographic protocol is a device to coordinate a number of principals, despite the presence of a malicious adversary. Exchange protocols in particular are intended to control changes in state for principals, i.e. changes in the set of values that they possess. An exchange protocol is fair if it ensures that the state changes are balanced: If one participant obtains a new possession via the protocol, then all other participants do, too. Fair exchange protocols require some mechanism to ensure progress: If some participants obtain their values first and stop, the other participants can continue a branch of the protocol to obtain theirs, typically with the help of a trusted third party.

In this paper, we enrich the strand space model to support reasoning about fair exchange protocols. First, we use multiset rewriting to allow strands to modify the state, and to allow the state to control how strands execute. Second, we allow progress assumptions,

stipulating that some channels are resilient, and guaranteed to deliver messages, and that some principals (e.g. trusted principals) are guaranteed not to stop at critical steps.

A recent fair exchange protocol (Cederquist, Dashti, and Mauw) provides an illustration. The strand space execution model -- which is partially ordered -- gives a logically simpler treatment of correctness conditions than previous linear trace approaches, since no fair execution assumptions are required.

Chris Heunen. Semimodule enrichment

Abstract. A category with biproducts is enriched over commutative monoids of addition. A category with tensor products is enriched over scalar multiplication actions. A symmetric monoidal category with biproducts is enriched over semimodules. We show that these changes of enrichment are functorial, and use them to make precise the intuition that ``compact objects are finite-dimensional''.

Achim Jung, M. Andrew Moshier and Steve Vickers. Presenting dcpo algebras

Abstract. We show how poset algebras can be freely completed to dcpo algebras, subject to a set of prescribed identifications.

Daniel Leivant. Propositional dynamic logic with quantifiers over programs

Abstract. It is well known that the propositional mu-calculus can be embedded in PDL with quantifiers over propositions. Here we consider PDL with quantifiers over programs. The difference between the two issues is significant: quantification over programs corresponds to quantifying over *binary* relations in Kripke structures, whereas quantification over propositions corresponds to quantification over unary relations.

Paul Blain Levy. Global state considered helpful

Abstract. Reynolds' view of a storage cell as an "expression-acceptor pair" has been widely used by researchers. We present a different way of organizing semantics of state, and in particular game semantics, by adding a "global state" zone to typing contexts. This has the following advantages.

Firstly, it causes the "good variable" equations for references to be validated, and also the noninterference equations between distinct references, as enumerated by Plotkin and Power.

Secondly, it gives a cleaner categorical structure based on the configurations (state + program) used to describe operational semantics.

Thirdly, it leads to a simpler proof that the game semantics is sound and adequate with respect to the operational semantics.

Keye Martin and Prakash Panangaden. A technique for verifying measurements

Abstract. We give a technique that can be used to prove that a given function is a measurement. We demonstrate its applicability by using it to resolve three notoriously difficult cases: capacity in information theory, entropy in quantum mechanics and global time in general relativity. We then show that this technique provides a new and surprising characterization of measurement. Thus, in principle, it can \em always \em be used.

Marino Miculan. A categorical model of Fusion calculus

Abstract. We provide a categorical presentation of the Fusion calculus. More precisely, we ﬁrst describe the syntax as the initial algebra of a signature functor and the semantics of processes as coalgebras of a “behaviour” endofunctor, over a suitable category of presheaves. The coalgebraic bisimulations induced by this functor is closed under substitutions (hence it is a congruence), and corresponds to hyperequivalence. Then, we provide a bialgebraic model of Fusion by modelling the rules of original labelled transition system as abstract categorical rules. As a consequence, we get a semantics for the Fusion calculus which is both compositional and fully abstract, that is, two processes have the same semantics iﬀ they are bisimilar, that is, hyperequivalent.

Aleksandar Nanevski. Semantics and dynamics

Abstract. Two main properties make type systems an effective and scalable formal method. First, important classes of programming errors are eliminated by statically enforcing the correct use of values. Second, types facilitate modular software development by serving as specifications of program components, while hiding the component's actual implementation. Implementations with the same type can be interchanged, thus facilitating software reuse and evolution.

Mainstream type systems focus on specifying relatively simple properties that admit type inference and checking with little or no input from the programmer. Unfortunately, this leaves a number of properties, including data structure invariants and API protocols outside of their reach, and also restricts the practical programming features that can be safely supported. For example, most simply-typed languages cannot safely allow low-level operations such as pointer arithmetic or explicit memory management.

In this talk, I will describe Hoare Type Theory (HTT) which combines dependent types of a system like Coq with features for specification and verification of low-level stateful operations in the style of Hoare Logic. The specification is performed via types -- which we call Hoare types -- thus also guaranteeing that the system is modular in nature.

Such a combination is desirable for several reasons. On the type-theoretic side, it makes it possible to integrate stateful behavior into dependent type theories that have so far been purely functional. On the Hoare Logic side, it makes is possible to use the higher-order data abstraction and information hiding mechanisms of type theory, which are essential for scaling any kind of verification effort. For example, by combining type-theoretic abstractions with Hoare types, we are able to capture the specifications for local higher-order state, as well as encode the main ideas from Separation Logic.

From the technical standpoint, it is interesting that the design of HTT relates in an essential way some of the most venerable ideas from programming language theory such as Dijkstra's predicate transformers, Curry-Howard isomorphism and monads.

I will discuss the implementation of HTT (called Y-not) which is currently under way, as well as the possibilities for scaling HTT to support further programming features.

This is joint work with Greg Morriset, Lars Birkedal, Amal Ahmed, Rasmus Petersen, Avi Shinnar and Paul Govereau.

Benjamin Pierce. Types Considered Harmful

Abstract. A long-time advocate of fancy type systems reconsiders his position.

Gordon Plotkin and John Power. Tensors of Comodels and Models for Operational Semantics

Abstract. In seeking a uniﬁed study of computational eﬀects, one must take account of the

coalgebraic structure of state in order to give a general operational semantics agreeing with the standard one for state. Axiomatically, one needs a countable Lawvere theory L, a comodel C , typically the ﬁnal one, and a model M , typically free; one then seeks a tensor C ⊗ M of the comodel with the model that allows operations to ﬂow between the two. We describe such a tensor implicit in the abstract category theoretic literature, explain its signiﬁcance for computational eﬀects, and calculate it in leading classes of examples, primarily involving state.

Andreas Rossberg. Dynamic Translucency with Abstraction Kinds

Abstract. When a module language is combined with forms of non-parametric type analysis, abstract types require an opaque dynamic representation in order to maintain abstraction safety. As an idealisation of such a module language, we present a foundational calculus that combines higher-order type generation, modelling type abstraction, with singleton kinds, modelling translucency. In this calculus, type analysis can dynamically exploit translucency, without breaking abstraction.

Abstract types are classified by a novel notion of abstraction kinds. These are analogous to singletons, but instead of inducing equivalence they induce an isomorphism that is witnessed by explicit type coercions on the term level.

To encompass higher-order forms of translucent abstraction, we give an account for higher-order coercions in a rich type system with higher-order polymorphism and dependent kinds. The latter necessitate the introduction of an analogous notion of kind coercions on the type level. Finally, we give an abstraction-safe encoding of ML-style module sealing in terms of higher-kinded type generation and higher-order coercion.

Adam Scriven. A Functional Algorithm for Exact Real Integration with Invariant Measures

Abstract In this study we develop an algorithm for exact real integration over a class of self-similar spaces/measures known as invariant spaces/measures. We construct the algorithm in a lazy functional language, and prove its correctness on all computable invariant spaces in the denotational semantic domain. Our work generalises an algorithm developed by Alex Simpson for exact Riemann integration over the real line. We implement the algorithm in Haskell and give some preliminary experimental results.

Alan Sexton and Hayo Thielecke. Reasoning about B+ Trees with Operational Semantics and Separation Logic

Abstract B+ trees are the most widely used file index structure in database systems, and the ``post-and-grow'' idea, which is the source of their success, is the basis of many other index structures that are more complex. Such complexity has lead to difficulties in specifying such structures and proving their correctness. In this paper, we apply two techniques from programming language theory to B+ trees: operational semantics, in the form of an abstract machine, and separation logic. We use an abstract machine to give a precise and tractable formalisation of the operations on B+ trees. Separation logic is then used to formalise a data structure invariant for B+ trees and to establish correctness by showing that the invariant is preserved by the operations. As usual in separation logic, frame laws are essential for keeping the reasoning local. In our setting, that means that we concentrate on the subtree reached from the top of the stack of the abstract machine, while the remainder of the B+ tree stays invariant. We believe that these techniques extend to the more complex index structures as well.

Carsten Varming and Lars Birkedal. Higher-Order Separation Logic in Isabelle/HOLCF

Abstract. We formalize higher-order separation logic for a first-order imperative language with procedures and local variables in Isabelle/HOLCF. The assertion language is modeled in such a way that one may use any theory defined in Isabelle/HOLCF to construct assertions, e.g., primitive recursion, least or greatest fixed points etc. The higher-order logic ensures that we can show non-trivial algorithms correct without having to extend the semantics of the language as was done previously in verifications based on first-order separation logic \cite{Birkedal2004Local,Yang2000Example}. We provide non-trivial examples to support this claim and to show how the higher-order logic enables natural assertions in specifications. To support abstract reasoning we have implemented rules for representation hiding and data abstraction as seen in \cite{Biering2007BIhyperdoctrines}.

The logic is represented as lemmas for reasoning about the denotational semantics of the programming language. This follows the definitional approach common in HOL theorem provers, i.e., the soundness of our model only relies on the soundness of Isabelle/HOL \cite{Gordon1991Introduction}.

We use our formalization to give a formally verified proof of Cheney's copying garbage collector \cite{Cheney1970Nonrecursive} using a tagged representation of objects. The proof generalizes the results in \cite{Birkedal2004Local}. The proof

uses an encoding of the separation logic formula `this(h)' to capture the heap from before the garbage collection and thus shows another novel use of higher-order separation logic.

Marcelo Fiore. Algebraic Theories and Equational Logics

Abstract. The tutorial is organised in two parts. In the first part, I will examine the basic theory of universal algebra; presenting the syntax and semantics of algebraic theories and their associated equational logic from the general perspective of categorical algebra. In the second part, I will show how to enrich the setting to provide an algebraic treatment of binding operators and substitution on top of which I will discuss second-order algebraic theories and their associated equational logic.

Nicola Gambino. Categorical and homotopical structures in dependent type theory

Abstract. The tutorial will offer an overview of the current state of research in the semantics of dependent type theories. We begin by reviewing the syntax of dependent type theories. We then explain its standard category-theoretic semantics based on Lawvere's notion of hyperdoctrine. Finally, we explain the recent applications of homotopical algebra to the semantics of identity types..

Pieter Hofstra. Introduction to abstract computability

Abstract. After briefly reviewing some of the history of various generalizations of traditional computability theory, I will present a categorical framework in which one can develop elementary recursion theory. It is also suitable for studying the connections between various notions of computability, and it comprises several well-known formalisms

such as (models of) untyped lambda calculus, combinatory logic and abstract computation domains. My primary goal is to give an introduction to this categorical setting, to provide various examples and to give the audience a feel for its possibilities and limitations. I will also exhibit some close connections to various other areas, such the theory of partial combinatory algebras and realizability, and explain how the problem of comparing different notions of computation may be handled.

Peter Selinger. Categorical models of quantum computation

Abstract. The semantics of quantum computation gives rise to some interesting categorical descriptions. I will focus on the semantics of higher-order quantum computation, and survey the state of the art in this area.

Meeting Talks