1,205 papers · page 15 of 61
Developing a theory of bisimulation in higher-order languages can be hard. Particularly challenging can be: (1) the proof of congruence, as well as enhancements of the bisimulation proof method with “up-to context” techniques, and (2) obtaining definitions and results that scale …
Type constraints express subtype relationships between the types of program expressions, for example, those relationships that are required for type correctness. Type constraints were originally proposed as a convenient framework for solving type checking and type inference probl…
Compositional theories are crucial when designing large and complex systems from smaller components. In this work we propose such a theory for synchronous concurrent systems. Our approach follows so-called interface theories, which use game-theoretic interpretations of compositio…
The language JavaGI extends Java 1.5 conservatively by a generalized interface mechanism. The generalization subsumes retroactive and type-conditional interface implementations, binary methods, symmetric multiple dispatch, interfaces over families of types, and static interface m…
Floyd--Hoare logic is a foundation of axiomatic semantics of classical programs, and it provides effective proof techniques for reasoning about correctness of classical programs. To offer similar techniques for quantum program verification and to build a logical foundation of pro…
Typed Assembly Languages (TALs) are used to validate the safety of machine-language programs. The Foundational Proof-Carrying Code project seeks to verify the soundness of TALs using the smallest possible set of axioms: the axioms of a suitably expressive logic plus a specificati…
The goal of feature-oriented programming (FOP) is to modularize software systems in terms of features. A feature refines the content of a base program. Both base programs and features may contain various kinds of software artifacts, for example, source code in different languages…
Over the last seven years, we have developed static-analysis methods to recover a good approximation to the variables and dynamically allocated memory objects of a stripped executable, and to track the flow of values through them. The article presents the algorithms that we devel…
Permissions specify mutable state that can be accessed by a program. Fractions distinguish write access (1) from read access (any smaller fraction). Nesting can model object invariants and ownership. Fractional permissions provides a foundation the meaning of many of access-based…
Although register allocation is critical for performance, the implementation of register allocation algorithms is difficult, due to the complexity of the algorithms and target machine architectures. It is particularly difficult to detect register allocation errors if the output c…
This article addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fields, that is, interprocedural shape analysis . The article makes three contributions. — It introduces…
By studying the behavior of several programs that crash due to memory errors, we observed that locating the errors can be challenging because significant propagation of corrupt memory values can occur prior to the point of the crash. In this article, we present an automated appro…
Traditional static type systems are effective for verifying basic interface specifications. Dynamically checked contracts support more precise specifications, but these are not checked until runtime, resulting in incomplete detection of defects. Hybrid type checking is a synthesi…
We propose a type system for lock-freedom in the π-calculus, which guarantees that certain communications will eventually succeed. Distinguishing features of our type system are: it can verify lock-freedom of concurrent programs that have sophisticated recursive communication str…
Pluggable types enable users to enforce multiple type systems in one programming language. We have developed a suite of tools, called the JavaCOP framework, that allows developers to create pluggable type systems for Java. JavaCOP provides a simple declarative language in which p…
La Dolce Vita at TOPLASDear TOPLAS authors, reviewers, and readers, The TOPLAS community is working in exciting times for research in programming languages and programming systems.As every aspect of life becomes more dependent on computer applications and systems, what programmin…
No abstract available.
Computational grids have an enormous potential to provide compute power. However, this power remains largely unexploited today for most applications, except trivially parallel programs. Developing parallel grid applications simply is too difficult. Grids introduce several problem…
This article concerns mechanisms for maintaining the value of an instrumentation relation (also known as a derived relation or view ), defined via a logical formula over core relations, in response to changes in the values of the core relations. It presents an algorithm for trans…
We present a type system for linear constraints over the reals intended for reasoning about the input-output directionality of variables. Types model the properties of definiteness, range width or approximation, lower and upper bounds of variables in a linear constraint. Several …