Publications

Reverse Hoare Logic

Reverse Hoare Logic, Edsko de Vries and Vasileios Koutavas. In G. Barthe, A. Pardo and G. Schneider (Ed.): SEFM 2011, LNCS 7041, pp. 155-171, 2011. Paper 

Abstract: We present a novel Hoare-style logic, called Reverse Hoare Logic, which can be used to reason about state reachability of imperative programs. This enables us to give natural specifications to randomized (deterministic or nondeterministic) algorithms. We give a proof system for the logic and use this to give simple formal proofs for a number of illustrative examples. We define a weakest postcondition calculus and use this to show that the proof system is sound and complete.

Transactions

Liveness of Communicating Transactions (Extended Abstract), Edsko de Vries, Vasileios Koutavas and Matthew Hennessy. In K. Ueda (Ed.): APLAS 2010, LNCS 6461, pp. 392—407, 2010. Paper 

Abstract: We study liveness and safety in the context of CCS extended with communicating transactions, a construct we recently proposed to model automatic error recovery in distributed systems. We show that fair-testing and may-testing capture the right notions of liveness and safety in this setting, and argue that must-testing imposes too strong a requirement in the presence of transactions. We develop a sound and complete theory of fair-testing in terms of CCS-like tree failures and show that, compared to CCS, communicating transactions provide increased distinguishing power to the observer. We also show that weak bisimilarity is a sound, though incomplete, proof technique for both may- and fair-testing. To the best of our knowledge this is the first semantic treatment of liveness in the presence of transactions. We exhibit the usefulness of our theory by proving illuminating liveness laws and simple but non-trivial examples.

Communicating Transactions (Extended Abstract), Edsko de Vries, Vasileios Koutavas and Matthew Hennessy. In Paul Gastin and François Laroussinie (Eds.): CONCUR 2010, LNCS 6269, pp. 569-583, 2010. Paper , Technical appendix with proofs , Slides

Abstract: We propose a novel language construct called communicating transactions, obtained by dropping the isolation requirement from classical transactions, which can be used to model automatic error recovery in distributed systems. We extend CCS with this construct and give a simple semantics for the extended calculus, called TransCCS. We develop a behavioural theory which is sound and complete with respect to the may-testing preorder, and use it to prove interesting laws and reason compositionally about example systems. Finally, we prove that communicating transactions do not increase the observational power of processes; thus CCS equivalences are preserved in the extended language.

Resource Management in the Pi-Calculus

Uniqueness Typing for Resource Management in Message-Passing Concurrency, Edsko de Vries, Adrian Francalanza and Matthew Hennessy. In Journal of Logic and Computation (to appear). Paper 

Abstract: We view channels as the main form of resources in a message-passing programming paradigm. These channels need to be carefully managed in settings where resources are scarce. To study this problem, we extend the \pic with primitives for channel allocation and deallocation and allow channels to be reused to communicate values of different types. Inevitably, the added expressiveness increases the possibilities for runtime errors. We define a substructural type system which combines uniqueness typing and affine typing to reject these ill-behaved programs.

The above journal paper is an expanded version of the conference paper, below:

Reasoning about Explicit Resource Management (Abstract), Edsko de Vries, Adrian Francalanza and Matthew Hennessy. In PLACES 2011. Paper 

Abstract: We define a pi-calculus variant with a costed semantics where channels are treated as resources that must explicitly be allocated before they are used and can be deallocated when no longer required. We use a substructural type system tracking permission transfer to construct compositional proof techniques for comparing behaviour and resource usage efficiency of concurrent processes.

Uniqueness Typing for Resource Management in Message-Passing Concurrency, Edsko de Vries, Adrian Francalanza and Matthew Hennessy. In M. Florido and I. Mackie (Eds.): First International Workshop on Linearity (LINEARITY 2009). Electronic Proceedings in Theoretical Computer Science, 22, 2010, pp. 26-37. Paper , Technical appendix with proofs , Slides

Abstract: We view channels as the main form of resources in a message-passing programming paradigm. These channels need to be carefully managed in settings where resources are scarce. To study this problem, we extend the pi calculus with primitives for channel allocation and deallocation and allow channels to be reused to communicate values of different types. Inevitably, the added expressivity increases the possibilities for runtime errors. We define a substructural type system which combines uniqueness typing and affine typing to reject these ill-behaved programs.

On Uniqueness Typing

Making Uniqueness Typing Less Unique, Edsko de Vries, PhD thesis, Trinity College Dublin, Ireland, 2008. Printable version , Hyperlinked version for screen reading

Summary: The PhD thesis contains expanded versions of the three papers mentioned below (Uniqueness Typing Redefined, Equality Based Uniqueness Typing and Uniqueness Typing Simplified) and an in-depth discussion of avenues for future work, as well as a detailed introduction to uniqueness typing and substructural logics in general (including a comparison to Haskell's monadic approach) and a survey of related work in the area.

The thesis (above) contains expanded and improved versions of the papers listed below and should generally be preferred.

Uniqueness Typing Simplified, Edsko de Vries, Rinus Plasmeijer, and David Abrahamson. In Olaf Chitil, Zoltán Horváth and Viktória Zsók (Eds.): IFL 2007, LNCS 5083, pp. 201-218, 2008. Paper , Slides

Abstract: We present a uniqueness type system that is simpler than both Clean's uniqueness system and the system we proposed previously. The new type system is straightforward to implement and add to existing compilers, and can easily be extended with advanced features such as higher rank types and impredicativity. We describe our implementation in Morrow, an experimental functional language with both these features. Finally, we prove soundness of the core type system with respect to the call-by-need lambda calculus.

Uniqueness Typing Simplified—Technical Appendix, Edsko de Vries. Technical report TCD-CS-2008-19. Report , Coq sources

Abstract: This technical report is an appendix to Uniqueness Typing Simplified, in which we show how uniqueness typing can be simplified by treating uniqueness attributes as types of a special kind, allowing arbitrary boolean expressions as attributes, and avoiding subtyping. In the paper, we define a small core uniqueness type system (a derivative of the simply typed lambda calculus) that incorporates these ideas. We also outline how soundness with respect to the call-by-need semantics can be proven, but we do not give any details. This report describes the entire proof, which is written using the proof assistant Coq.

Equality Based Uniqueness Typing, Edsko de Vries, Rinus Plasmeijer, and David Abrahamson. Presented at TFP 2007. Paper , Slides , Prototype

Abstract: We define a uniqueness type system for the core lambda calculus which, unlike Clean's uniqueness system and the system we proposed in a previous paper, does not involve inequalities. We claim that this makes the type system sufficiently similar to the Hindley/Milner type system that standard type inference algorithms can be applied, and that it can easily be modified to incorporate modern extensions such as arbitrary rank types and generalized algebraic data types. We substantiate this claim by sketching out how such a system would be defined.

Uniqueness Typing Redefined, Edsko de Vries, Rinus Plasmeijer, and David Abrahamson. In Zoltán Horváth, Viktória Zsók, and Andrew Butterfield (Eds.): IFL 2006, LNCS 4449, pp. 181-198, 2007. Paper , Slides

Abstract: We modify Clean's uniqueness type system in two ways. First, where in Clean functions that are partially applied to a unique argument are necessarily unique (they cannot lose their uniqueness), we just require that they must be unique when applied. This ultimately makes subtyping redundant. Second, we extend the type system to allow for higher rank types. To be able to do this, we explicitly associate type constraints (attribute inequalities) with type schemes. Consequently, types in our system are much more precise about constraint propagation.

On Polytypic Programming

Formal Polytypic Programs and Proofs, Wendy Verbruggen, Edsko de Vries and Arthur Hughes. Journal of Functional Programming, Volume 20, Special Issue 3-4, pp 213-269. Paper 

Abstract: The aim of our work is to be able to do fully formal (machine verified) proofs over Generic Haskell-style polytypic programs. In order to achieve this goal, we embed polytypic programming in the proof assistant Coq and provide an infrastructure for polytypic proofs. Polytypic functions are reified within Coq as a datatype PolyFn and can be specialized by applying an ordinary (dependently typed) function specTerm. Polytypic functions are thus first class citizens and can be passed as arguments or returned as results. Likewise, we reify polytypic proofs as a datatype PolyProof, and provide a lemma specProof (analogous to specTerm) that a polytypic proof can be specialized to any datatype in the universe. The correspondence between polytypic functions and their polytypic proofs is very clear: programmers need to give proofs for, and only for, the same cases that they need to give instances for when they define the polytypic function itself. Finally, we discuss how we can write (co)recursive functions and do (co)recursive proofs in a similar way that recursion is handled in Generic Haskell.

Polytypic Properties and Proofs in Coq, Wendy Verbruggen, Edsko de Vries and Arthur Hughes. In WGP '09: Proceedings of the 2009 ACM SIGPLAN workshop on Generic programming, Edinburgh, UK. August 2009, pp. 1-12. Paper , Coq source

Abstract: We formalize proofs over Generic Haskell-style polytypic programs in the proof assistant Coq. This makes it possible to do fully formal (machine verified) proofs over polytypic programs with little effort. Moreover, the formalization can be seen as a machine verified proof that polytypic proof specialization is correct with respect to polytypic property specialization.

Polytypic Programming in Coq, Wendy Verbruggen, Edsko de Vries, and Arthur Hughes. In Ralf Hinze. (Ed.): ACM SIGPLAN Workshop on Generic Programming 2008, pp. 49-60. Paper , Coq source

Abstract: The aim of our work is to provide an infrastructure for formal proofs over Generic Haskell-style polytypic programs. For this goal to succeed, we must have a definition of polytypic programming which is both fully formal and as close as possible to the definition in Generic Haskell. In this paper we show a formalization in the proof assistant Coq of type and term specialization. Our definition of term specialization can be interpreted as a formal proof that the result of term specialization has the type computed by type specialization.

Related to phc

A Practical Solution for Achieving Language Compatibility in Scripting Language Compilers, Paul Biggar, Edsko de Vries, David Gregg. In Science of Computer Programming, ISSN 0167-6423. Available online 8 February 2011. Paper

Abstract: Although scripting languages have become very popular, even mature scripting language implementations remain interpreted. Several compilers and reimplementations have been attempted, generally focusing on performance.

Based on our survey of these reimplementations, we determine that there are three important features of scripting languages that are difficult to compile or reimplement. Since scripting languages are defined primarily through the semantics of their original implementations, they often change semantics between releases. They provide C APIs, used both for foreign-function interfaces and to write third-party extensions. These APIs typically have tight integration with the original implementation, and are used to provide large standard libraries, which are difficult to re-use, and costly to reimplement. Finally, they support run-time code generation. These features make it difficult to design a fully compatible compiler.

We present a technique to support these features in an ahead-of-time compiler for PHP. Our technique uses the original PHP implementation through the provided C API, both in our compiler and in our generated code. We support all of these important scripting language features. Additionally, our approach allows us to automatically support limited future language changes. We present a discussion and performance evaluation of this technique.

The above journal paper is an expanded version of the conference paper, below:

A Practical Solution for Scripting Language Compilers, Paul Biggar, Edsko de Vries and David Gregg. In SAC '09: Proceedings of the 2009 ACM Symposium on Applied Computing, (March 2009). Paper 

Abstract: Although scripting languages are becoming increasingly popular, even mature scripting language implementations remain interpreted. Several compilers and reimplementations have been attempted, generally focusing on performance.

Based on our survey of these reimplementations, we determine that there are three important features of scripting languages that are difficult to compile or reimplement. Since scripting languages are defined primarily through the semantics of their original implementations, they often change semantics between releases. They provide large standard libraries, which are difficult to re-use, and costly to reimplement. They provide C APIs, used both for foreignfunction- interfaces and to write third-party extensions. These APIs typically have tight integration with the original implementation. Finally, they support run-time code generation. These features make the important goal of correctness difficult to achieve.

We present a technique to support these features in an ahead-oftime compiler for PHP. Our technique uses the original PHP implementation through the provided C API, both in our compiler, and an our generated code. We support all of these important scripting language features, particularly focusing on the correctness of compiled programs. Additionally, our approach allows us to automatically support limited future language changes. We present a discussion and performance evaluation of this technique, which has not previously been published.

Processing ASTs in C++: maketea, Edsko de Vries, John Gilbert and David Abrahamson. Unpublished manuscript. (paper)

Abstract: We present maketea, a tool which generates a C++ infrastructure for processing ASTs based on an object oriented context free grammar. The generated code includes a class hierarchy for storing ASTs with support for cloning, equality checking, pattern matching, a general visitor API and a transformation API. The tool is available under an open source license and can be downloaded from www.maketea.org.

Design and Implementation of a PHP Compiler Front-end, Edsko de Vries, John Gilbert. Technical Report TCD-CS-2007-47, Trinity College Dublin. Report

Abstract: This technical report describes the design and implementation of a front-end for phc, the open source PHP compiler. This front-end provides an excellent basis for developing tools which process PHP source code, and consists of a well-defined Abstract Syntax Tree (AST) specification for the PHP language, a lexical analyser and parser which construct the AST for a given script, and a visitor and transformation API for manipulating these ASTs.