POPL
2012
ACM
12 years 8 months ago
2012
ACM
Despite recent successes, large-scale proof development within proof assistants remains an arcane art that is extremely timeconsuming. We argue that this can be attributed to two ...
POPL
2012
ACM
12 years 8 months ago
2012
ACM
JavaScript has become the most widely used language for clientside web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading t...
POPL
2012
ACM
12 years 8 months ago
2012
ACM
Gradual typing lets programmers evolve their dynamically typed programs by gradually adding explicit type annotations, which confer benefits like improved performance and fewer r...
POPL
2012
ACM
12 years 8 months ago
2012
ACM
There has been great progress in recent years on developing effective techniques for reasoning about program equivalence in ML-like languages—that is, languages that combine fea...
POPL
2012
ACM
12 years 8 months ago
2012
ACM
Interpolation is an important technique in verification and static analysis of programs. In particular, interpolants extracted from proofs of various properties are used in invar...
POPL
2012
ACM
12 years 8 months ago
2012
ACM
Functional reactive programming (FRP) is an elegant and successful approach to programming reactive systems declaratively. The high levels of abstraction and expressivity that mak...
POPL
2012
ACM
12 years 8 months ago
2012
ACM
Since software systems are becoming increasingly more concurrent and distributed, modeling and analysis of interactions among their components is a crucial problem. In several app...
POPL
2012
ACM
12 years 8 months ago
2012
ACM
Data races are among the most reliable indicators of programming errors in concurrent software. For at least two decades, Lamport’s happens-before (HB) relation has served as th...
POPL
2012
ACM
12 years 8 months ago
2012
ACM
Differential privacy is a notion of confidentiality that protects the privacy of individuals while allowing useful computations on their private data. Deriving differential priva...
POPL
2012
ACM
12 years 8 months ago
2012
ACM
We show how to combine a general purpose type system for an existing language with support for programming with binders and contexts by refining the type system of ML with a rest...