POPL
2007
ACM
15 years 23 days ago
2007
ACM
There is a clear intuitive connection between the notion of leakage of information in a program and concepts from information theory. This intuition has not been satisfactorily pi...
POPL
2007
ACM
15 years 23 days ago
2007
ACM
We present an internal language with equivalent expressive power to Standard ML, and discuss its formalization in LF and the machine-checked verification of its type safety in Twe...
POPL
2007
ACM
15 years 23 days ago
2007
ACM
XML programming involves idioms for expressing `structure shyness' such as the descendant axis of XPath or the default templates of XSLT. We initiate a discussion of the rela...
POPL
2007
ACM
15 years 23 days ago
2007
ACM
Pushdown Systems (PDSs) has become an important paradigm for program analysis. Indeed, recent work has shown a deep connection between inter-procedural dataflow analysis for seque...
100
click to vote
POPL
2007
ACM
15 years 23 days ago
2007
ACM
A memory leak in a garbage-collected program occurs when the program inadvertently maintains references to objects that it no longer needs. Memory leaks cause systematic heap grow...
POPL
2007
ACM
15 years 23 days ago
2007
ACM
An asynchronous program is one that contains procedure calls which are not immediately executed from the callsite, but stored and "dispatched" in a non-deterministic ord...
POPL
2007
ACM
15 years 23 days ago
2007
ACM
In this paper, we propose a new algorithm for proving the validity or invalidity of a pre/postcondition pair for a program. The algorithm is motivated by the success of the algori...
POPL
2007
ACM
15 years 23 days ago
2007
ACM
114
click to vote
POPL
2007
ACM
15 years 23 days ago
2007
ACM
We propose a new technique for hardware synthesis from higherorder functional languages with imperative features based on Reynolds's Syntactic Control of Interference. The re...
POPL
2007
ACM
15 years 23 days ago
2007
ACM
We introduce lock allocation, an automatic technique that takes a multi-threaded program annotated with atomic sections (that must be executed atomically), and infers a lock assig...