Browse Proceedings

We introduce the <em>blame calculus</em> , which adds the notion of blame from Findler and Felleisen's <em>contracts</em> to a system similar to Siek and Taha's <em>gradual types</em> and Flanagan's <em>hybrid types</em> . We characterise where positive ...

This paper explores the surprisingly rich design space for the simply typed lambda calculus with casts and a dynamic type. Such a calculus is the target intermediate language of the gradually typed lambda calculus but it is also interesting in its own ...

Just as some functions have uniform behavior over distinct types, other functions have uniform behavior over distinct arities. These variable-arity functions are widely used in scripting languages such as Scheme and Python. Statically typed languages ...

This paper studies inductive definitions involving binders, in which aliasing between free and bound names is permitted. Such aliasing occurs in informal specifications of operational semantics, but is excluded by the common representation of binding as ...

In a 1980 paper entitled "Using Category Theory to Design Conversions and Generic Operators", the author showed how the concepts of category theory can guide the design of a programming language to avoid anomalies in the interaction of implicit ...

During the last two decades, monads have become an indispensable tool for structuring functional programs with computational effects. In this setting, the mathematical notion of a monad is extended with operations that allow programmers to manipulate ...

We present an algebraic treatment of exception handlers and, more generally, introduce handlers for other computational effects representable by an algebraic theory. These include nondeterminism, interactive input/output, concurrency, state, time, and ...

Structural subtyping is popular in research languages, but all mainstream object-oriented languages use nominal subtyping. Since languages with structural subtyping are not in widespread use, the empirical questions of whether and how structural ...

Variant parametric types represent the successful integration of subtype and parametric polymorphism to support a more flexible subtyping for Java like languages. A key feature that helps strengthen this integration is the use-site variance. Depending ...

Ownership types characterize the topology of objects in the heap, through a characterization of the context to which an object belongs. They have been used to support reasoning, memory management, concurrency, <em>etc.</em> Subtyping is traditionally ...

Reference attribute grammars are a powerful formalism for concisely specifying and implementing static analyses. While they have proven their merit in practical applications, no attempt has so far been made to rigorously verify correctness properties of ...

We describe the mechanisation of an SLR parser produced by a parser generator, covering background properties of context-free languages and grammars, as well as the construction of an SLR automaton. Among the various properties proved about the parser ...

The context-free language (CFL) reachability problem is well known and studied in computer science, as a fundamental problem underlying many important static analyses such as points-to-analysis. Solving the CFL reachability problem in the general case ...

Hofmann and Jost have presented a heap space analysis [1] that finds linear space bounds for many functional programs. It uses an amortised analysis: assigning hypothetical amounts of free space (called potential) to data structures in proportion to ...

The magnitude and dramatic consequences of the current "financial crisis" are publicly well documented. Even non professionals may read in, say, newspapers about notions like "derivatives", "over the counter deals", "complexity of contracts", "...

Tools for analysing secure information flow are almost exclusively based on ideas going back to Denning's work from the 70's. This approach embodies an imperfect notion of security which turns a blind eye to information flows which are encoded in the ...

Gordon and Jeffrey have proposed a type and effect system for checking authenticity in cryptographic protocols. The type system reduces the protocol verification problem to the type checking problem, but protocols must be manually annotated with non-...

We develop a general method of proving contextual properties--including (but not limited to) observational equivalence, space improvement, and memory safety <em>under arbitrary contexts</em> --for programs in untyped call-by-value <em>***</em> -calculus ...

Concurrent data structures are usually designed to satisfy correctness conditions such as sequential consistency and linearizability. In this paper, we consider the following fundamental question: what guarantees are provided by these conditions for ...

The operational semantics of interactive systems is usually described by labeled transition systems. Abstract semantics is defined in terms of bisimilarity that, in the finite case, can be computed via the well-known <em>partition refinement algorithm</...

We present a type theory for analyzing concurrent multiparty interactions as found in service-oriented computing. Our theory introduces a novel and flexible type structure, able to uniformly describe both the internal and the interface behavior of ...

Orchestrators are descriptions at implementation level and may contain sensitive information that should be kept private. Consequently, orchestration languages come equipped with a notion of <em>abstract processes</em> , which enable the interaction ...

We generalise a theory of multiparty session types for the <em>***</em> -calculus through asynchronous communication subtyping, which allows partial commutativity of actions with maximal flexibility and safe optimisation in message choreography. A sound ...

Web services are distributed software components, that are decoupled from each other using interfaces with specified functional behaviors. However, such behavioral specifications are insufficient to demonstrate compliance with certain temporal non-...

Separation logic is a recent approach to the analysis of pointer programs in which resource separation is expressed with a logical connective in assertions that describe the state at any given point in the program. We extend this approach to express ...

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 ...

Advanced multi-threaded programs apply concurrency concepts in sophisticated ways. For instance, they use fine-grained locking to increase parallelism and change locking orders dynamically when data structures are being reorganized. This paper presents ...

Multithreaded programs are prone to errors caused by unintended interference between concurrent threads. This paper focuses on verifying that <em>deterministically-parallel</em> code is free of such thread interference errors. Deterministically-parallel ...