Science of Computer Programming

Message-passing is a key ingredient of concurrent programming. The purpose of this paper is to describe the equivalence between the proof theory, the categorical semantics, and term calculus of message-passing. In order to achieve this we introduce the ...

We present the left inverse of Reynolds' defunctionalization and we show its relevance to programming and to programming languages. We propose two methods to transform a program that is almost in defunctionalized form into one that is actually in ...

Instances of a polytypic or generic program for a concrete recursive type often exhibit a recursion scheme that is derived from the recursion scheme of the instantiation type. In practice, the programs obtained from a generic program are usually ...

Randomized algorithms are widely used for finding efficiently approximated solutions to complex problems, for instance primality testing and for obtaining good average behavior. Proving properties of such algorithms requires subtle reasoning both on ...

Support for generic programming consists of three essential ingredients: support for overloaded functions, a run-time type representation, and a generic view on data. Different approaches to datatype-generic programming occupy different points in this ...

Stepwise refinement is a crucial conceptual tool for system development, encouraging program construction via a number of separate correctness-preserving stages which ideally can be understood in isolation. A crucial conceptual component of security is ...

Refinement algebras are abstract algebras for reasoning about programs in a total correctness framework. We extend a reduct of von Wright's demonic refinement algebra with two operators for modelling enabledness and termination of programs. We show how ...