2,199 papers · page 57 of 110
Building concurrent shared-memory data structures is a notoriously difficult problem, and so the widespread move to multi-core and multi-processor hardware has led to increasing interest in language constructs that may make concurrent programming easier. One technique that has be…
Garbage collectors are notoriously hard to verify, due to their low-level interaction with the underlying system and the general difficulty in reasoning about reachability in graphs. Several papers have presented verified collectors, but either the proofs were hand-written or the…
Previous deforestation and supercompilation algorithms may introduce accidental termination when applied to call-by-value programs. This hides looping bugs from the programmer, and changes the behavior of a program depending on whether it is optimized or not. We present a superco…
We propose a new verification method for temporal properties of higher-order functional programs, which takes advantage of Ong's recent result on the decidability of the model-checking problem for higher-order recursion schemes (HORS's). A program is transformed to an HORS that g…
In this paper, we show how pattern matching can be seen to arise from a proof term assignment for the focused sequent calculus. This use of the Curry-Howard correspondence allows us to give a novel coverage checking algorithm, and makes it possible to give a rigorous correctness …
We present HML, a type inference system that supports full first-class polymorphism where few annotations are needed: only function parameters with a polymorphic type need to be annotated. HML is a simplification of MLF where only flexibly quantified types are used. This makes th…
Self-adjusting computation is an evaluation model in which programs can respond efficiently to small changes to their input data by using a change-propagation mechanism that updates computation by re-building only the parts affected by changes. Previous work has proposed language…
We study modular, automatic code generation from hierarchical block diagrams with synchronous semantics. Such diagrams are the fundamental model behind widespread tools in the embedded software domain, such as Simulink and SCADE. Code is modular in the sense that it is generated …
We propose a method for automatically generating abstract transformers for static analysis by abstract interpretation. The method focuses on linear constraints on programs operating on rational, real or floating-point variables and containing linear assignments and tests.
We propose F-zip, a calculus of open existential types that is an extension of System F obtained by decomposing the introduction and elimination of existential types into more atomic constructs. Open existential types model modular type abstraction as done in module systems. The …
Parallel programs on lists have been intensively studied. It is well known that associativity provides a good characterization for divide-and-conquer parallel programs. In particular, the third homomorphism theorem is not only useful for systematic development of parallel program…
This paper presents a type-based solution to the long-standing problem of object initialization. Constructors, the conventional mechanism for object initialization, have semantics that are surprising to programmers and that lead to bugs. They also contribute to the problem of nul…
This work develops an integrated approach to the verification of behaviourally rich programs, founded directly on operational semantics. The power of the approach is demonstrated with a state-of-the-art verification of a core piece of distributed infrastructure, involving network…
Multiprocessors are now dominant, but real multiprocessors do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have subtle relaxed (or weak) memory models, usually described only in ambiguous prose, leading t…
I shall present an extension of Moggi's computational metalanguage with primitives from linear logic, the enriched effect-calculus. Illustrative applications to side effects, continuations, nondeterminism and polymorphism will be considered. The talk is based on joint work with J…
Optimizations in a traditional compiler are applied sequentially, with each optimization destructively modifying the program to produce a transformed program that is then passed to the next optimization. We present a new approach for structuring the optimization phase of a compil…
PHP is a popular language for server-side applications. In PHP, assignment to variables copies the assigned values, according to its so-called copy-on-assignment semantics. In contrast, a typical PHP implementation uses a copy-on-write scheme to reduce the copy overhead by delayi…
A bidirectional transformation consists of a function get that takes a source (document or value) to a view and a function put that takes an updated view and the original source back to an updated source, governed by certain consistency conditions relating the two functions. Both…
Deadlock in multithreaded programs is an increasingly important problem as ubiquitous multicore architectures force parallelization upon an ever wider range of software. This paper presents a theoretical foundation for dynamic deadlock avoidance in concurrent programs that employ…
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…