文件名称：POPL 2011-Annual Symposium on Principles of Programming Languages 2011论文集
文件大小：27.76MB
文件格式：RAR
更新时间：2015-04-04 08:50:05
POPL ACM SIGPLAN SIGACT 2011
（我现在主要在CSDN上整理计算机安全、软件工程（可信软件）、系统及通信方面的论文及相关理论书籍，如果对这方面内容感兴趣，可以访问：http://qysh123.download.csdn.net/ 查看我上传的所有资料。内容比较多，需要大家人工手动查找。另外，资料顺序并不按照时间排列，只是想起来了就上传。CSDN这套系统不敢恭维，也请大家见谅。） 国际软件工程和编程语言界的*会议，POPL 2011年的会议论文集。POPL通常被认为是软件方面最*的国际会议之一，对程序语言、软件工程、可信软件等方面的研究者具有很重要的参考意义。 2011年POPL共收录包括Invited talk在内的18个session，共计52篇文章。奇怪的是，今年的论文集中有一个session叫做8.1 + 8.2，不知道是什么意思？ 另外值得一提的是，清华大学计算机系有一篇文章被2011年POPL收录：Bisimulation for quantum processes，在此恭喜相关老师和同学。
【文件预览】：
Invited talk
----Verified squared _ does critical software deserve verified tools.pdf(363KB)
----Robin Milner 1934--2010 _ verification, languages, and concurrency.pdf(275KB)
----The design of kodu _ a tiny visual programming language for children on the Xbox 360.pdf(476KB)
Complexity
----Complexity of pattern-based verification for multithreaded programs.pdf(609KB)
----Laws of order _ expensive synchronization in concurrent algorithms cannot be eliminated.pdf(484KB)
----Space overhead bounds for dynamic memory management with partial compaction.pdf(526KB)
Semantic models and translations
----A kripke logical relation between ML and assembly.pdf(574KB)
----A typed store-passing translation for general references.pdf(828KB)
----Step-indexed kripke models over recursive worlds.pdf(722KB)
Type abstractions
----Generative type abstraction and type-level computation.pdf(569KB)
----Blame for all.pdf(593KB)
----Correct blame for contracts _ no more scapegoating.pdf(587KB)
Synthesis
----Automating string processing in spreadsheets using input-output examples.pdf(695KB)
----Predicate abstraction and refinement for verifying multi-threaded programs.pdf(567KB)
----Geometry of synthesis III _ resource management through type inference.pdf(1.32MB)
Semi-automated verification
----Mathematizing C++ concurrency.pdf(523KB)
----Formal verification of object layout for c++ multiple inheritance.pdf(654KB)
----Relaxed-memory concurrency and verified compilation.pdf(510KB)
Static analysis
----Static analysis of multi-staged programs via unstaging translation.pdf(578KB)
----Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol.pdf(523KB)
----A parametric segmentation functor for fully automatic and scalable array content analysis.pdf(659KB)
Automata
----The tree width of auxiliary storage.pdf(510KB)
----Fresh-register automata.pdf(518KB)
----Vector addition system reachability problem _ a short self-contained proof.pdf(566KB)
Medley
----Bisimulation for quantum processes.pdf(476KB)
----EigenCFA _ accelerating flow analysis with GPUs.pdf(450KB)
----Safe nondeterminism in a deterministic-by-default parallel language.pdf(594KB)
Verification
----Decidable logics combining heap structures and data.pdf(554KB)
----Streaming transducers for algorithmic verification of single-pass list-processing programs.pdf(435KB)
----Verifying higher-order functional programs with pattern-matching algebraic data types.pdf(508KB)
8.1 + 8.2
----A technique for the effective and automatic reuse of classical compiler optimizations on multithreaded code.pdf(611KB)
Shape analysis
----Precise reasoning for programs using containers.pdf(742KB)
----A shape analysis for optimizing parallel graph programs.pdf(1.14MB)
----Calling context abstraction with shapes.pdf(806KB)
Point analyis
----Learning minimal abstractions.pdf(553KB)
----Pick your contexts well _ understanding object-sensitivity.pdf(466KB)
----Points-to analysis with efficient strong updates.pdf(589KB)
Compilation
----The essence of compiling with traces.pdf(601KB)
----Loop transformations _ convexity, pruning and optimization.pdf(470KB)
----Resourceable, retargetable, modular instruction selection using a machine-independent, type-based tiling of low-level intermediate code.pdf(465KB)
Algebra
----Symmetric lenses.pdf(887KB)
----Multivariate amortized resource analysis.pdf(1000KB)
----Regular expression containment _ coinductive axiomatization and computational interpretation.pdf(626KB)
Separation logic
----Expressive modular fine-grained concurrency specification.pdf(536KB)
----Modular reasoning for deterministic parallelism.pdf(512KB)
----A separation logic for refining concurrent objects.pdf(484KB)
Model checking
----Making prophecies with decision predicates.pdf(661KB)
----Delay-bounded scheduling.pdf(741KB)
----On interference abstractions.pdf(624KB)
Types
----Dynamic inference of static types for ruby.pdf(762KB)
----Dynamic multirole session types.pdf(570KB)
----Practical affine types.pdf(780KB)