POPL
2009
ACM
14 years 5 months ago
2009
ACM
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, t...
POPL
2009
ACM
14 years 5 months ago
2009
ACM
We present a proof calculus and method for the static verification of assertions and procedure specifications in shared-memory concurrent programs. The key idea in our approach is...
POPL
2009
ACM
14 years 5 months ago
2009
ACM
A concurrent data-structure implementation is considered nonblocking if it meets one of three following liveness criteria: waitfreedom, lock-freedom, or obstruction-freedom. Devel...
POPL
2009
ACM
14 years 5 months ago
2009
ACM
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 updat...
POPL
2009
ACM
14 years 5 months ago
2009
ACM
Transactional memory (TM) is a promising paradigm for concurrent programming. Whereas the number of TM implementations is growing, however, little research has been conducted to p...
POPL
2009
ACM
14 years 5 months ago
2009
ACM
The call-by-need lambda calculus provides an equational framework for reasoning syntactically about lazy evaluation. This paper examines its operational characteristics. By a seri...
POPL
2009
ACM
14 years 5 months ago
2009
ACM
Pointer analysis is a prerequisite for many program analyses, and the effectiveness of these analyses depends on the precision of the pointer information they receive. Two major a...
POPL
2009
ACM
14 years 5 months ago
2009
ACM
This paper presents a type-based solution to the long-standing problem of object initialization. Constructors, the conventional mechanism for object initialization, have semantics...
POPL
2009
ACM
14 years 5 months ago
2009
ACM
We present HML, a type inference system that supports full firstclass polymorphism where few annotations are needed: only function parameters with a polymorphic type need to be an...
POPL
2009
ACM
14 years 5 months ago
2009
ACM
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 verific...