文件名称：POPL 2012-Annual Symposium on Principles of Programming Languages 2012
文件大小：28.05MB
文件格式：RAR
更新时间：2015-05-30 15:19:28
ACM POPL 2012 编程语言 论文集
国际软件工程和编程语言界的*会议，POPL 2011年的会议论文集。POPL通常被认为是软件方面最*的国际会议之一，对程序语言、软件工程、可信软件等方面的研究者具有很重要的参考意义。在07年的计算机科学会议排名中，POPL名列第一，参见：http://citeseerx.ist.psu.edu/stats/venues 2012年POPL共收录包括Invited talk在内的18个session，共计48篇文章。 另外值得一提的是，中科大计算机学院有一篇文章被2012年POPL收录：A rely-guarantee-based simulation for verifying concurrent program transformations，在此恭喜相关老师和同学。
【文件预览】：
3.A security
----Defining code-injection attacks.pdf(678KB)
----Multiple facets for dynamic information flow.pdf(534KB)
Invited talk
----Meta-level features in an industrial-strength theorem prover.pdf(283KB)
----Programming languages for programmable networks.pdf(279KB)
1.A verification
----Freefinement.pdf(487KB)
----Towards a program logic for JavaScript.pdf(867KB)
----Underspecified harnesses and interleaved bugs.pdf(441KB)
6.A dynamic analysis
----Sound predictive race detection in polynomial time.pdf(466KB)
----Abstractions from tests.pdf(893KB)
8.A C C++ semantics
----A mechanized semantics for C++ object construction and destruction, with applications to resource management.pdf(677KB)
----Clarifying and compiling C C++ concurrency _ from C++11 to POWER.pdf(503KB)
----An executable formal semantics of C with applications.pdf(592KB)
2.B decision procedures
----Symbolic finite state transducers _ algorithms and applications.pdf(679KB)
----Constraints as control.pdf(647KB)
----Recursive proofs for inductive tree data-structures.pdf(522KB)
4.B mMechanized proofs
----Static and user-extensible proof checking.pdf(581KB)
----Run your research _ on the effectiveness of lightweight mechanization.pdf(754KB)
----Playing in the grey area of proofs.pdf(692KB)
5.B type theory
----On the power of coercion abstraction.pdf(715KB)
----Canonicity for 2-dimensional type theory.pdf(628KB)
----Algebraic foundations for effect-dependent optimisations.pdf(555KB)
4.A medley
----A compiler and run-time system for network programming languages.pdf(515KB)
----An abstract interpretation framework for termination.pdf(1.93MB)
----Nested refinements _ a logic for duck typing.pdf(643KB)
6.B names and binders
----Programming with binders and indexed data-types.pdf(613KB)
----Towards nominal computation.pdf(476KB)
7.B functional programming
----The ins and outs of gradual type inference.pdf(930KB)
----A unified approach to fully lazy sharing.pdf(656KB)
----Edit lenses.pdf(860KB)
1.B semantics
----Higher-order functional reactive programming in bounded space.pdf(684KB)
----The marriage of bisimulations and Kripke logical relations.pdf(561KB)
----Information effects.pdf(1.97MB)
2.A privacy and access control
----Access permission contracts for scripting languages.pdf(533KB)
----Probabilistic relational reasoning for differential privacy.pdf(552KB)
----A language for automatically enforcing privacy policies.pdf(627KB)
3.B complexity for concurrency
----Deciding choreography realizability.pdf(490KB)
----Analysis of recursively parallel programs.pdf(748KB)
Award presentation and interview
----Presentation of the SIGPLAN distinguished achievement award to Sir Charles Antony Richard Hoare, FRS, FREng, FBCS; and interview.pdf(316KB)
----Message of thanks _ on the receipt of the 2011 ACM SIGPLAN distinguished achievement award.pdf(332KB)
8.B type systems
----A type system for borrowing permissions.pdf(652KB)
----A type theory for probability density functions.pdf(497KB)
----Self-certification _ bootstrapping certified typecheckers in F with Coq.pdf(818KB)
7.A verified transformations
----A rely-guarantee-based simulation for verifying concurrent program transformations.pdf(510KB)
----Formalizing the LLVM intermediate representation for verified program transformations.pdf(714KB)
----Randomized accuracy-aware program transformations for efficient approximate computations.pdf(831KB)
5.A concurrency
----Verification of parameterized concurrent programs by modular reasoning about data and control.pdf(674KB)
----Resource-sensitive synchronization inference by abduction.pdf(710KB)
----Syntactic control of interference for separation logic.pdf(511KB)