POPL 2011
52 papers
- A kripke logical relation between ML and assembly
- A parametric segmentation functor for fully automatic and scalable array content analysis
- A separation logic for refining concurrent objects
- A shape analysis for optimizing parallel graph programs
- A technique for the effective and automatic reuse of classical compiler optimizations on multithreaded code
- A typed store-passing translation for general references
- Automating string processing in spreadsheets using input-output examples
- Bisimulation for quantum processes
- Blame for all
- Calling context abstraction with shapes
- Complexity of pattern-based verification for multithreaded programs
- Correct blame for contracts: no more scapegoating
- Decidable logics combining heap structures and data
- Delay-bounded scheduling
- Dynamic inference of static types for ruby
- Dynamic multirole session types
- EigenCFA: accelerating flow analysis with GPUs
- Expressive modular fine-grained concurrency specification
- Formal verification of object layout for c++ multiple inheritance
- Fresh-register automata
- Generative type abstraction and type-level computation
- Geometry of synthesis III: resource management through type inference
- Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated
- Learning minimal abstractions
- Loop transformations: convexity, pruning and optimization
- Making prophecies with decision predicates
- Mathematizing C++ concurrency
- Modular reasoning for deterministic parallelism
- Multivariate amortized resource analysis
- On interference abstractions
- Pick your contexts well: understanding object-sensitivity
- Points-to analysis with efficient strong updates
- Practical affine types
- Precise reasoning for programs using containers
- Predicate abstraction and refinement for verifying multi-threaded programs
- Regular expression containment: coinductive axiomatization and computational interpretation
- Relaxed-memory concurrency and verified compilation
- Resourceable, retargetable, modular instruction selection using a machine-independent, type-based tiling of low-level intermediate code
- Robin Milner 1934--2010: verification, languages, and concurrency
- Safe nondeterminism in a deterministic-by-default parallel language
- Space overhead bounds for dynamic memory management with partial compaction
- Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol
- Static analysis of multi-staged programs via unstaging translation
- Step-indexed kripke models over recursive worlds
- Streaming transducers for algorithmic verification of single-pass list-processing programs
- Symmetric lenses
- The design of kodu: a tiny visual programming language for children on the Xbox 360
- The essence of compiling with traces
- The tree width of auxiliary storage
- Vector addition system reachability problem: a short self-contained proof
- Verified squared: does critical software deserve verified tools?
- Verifying higher-order functional programs with pattern-matching algebraic data types