default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID39th POPL 2012: Philadelphia, Pennsylvania, USA
- John Field, Michael Hicks:
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012. ACM 2012, ISBN 978-1-4503-1083-3
Award presentation and interview
- Andrew P. Black, Peter W. O'Hearn:
Presentation of the SIGPLAN distinguished achievement award to Sir Charles Antony Richard Hoare, FRS, FREng, FBCS; and interview. 1-2 - Tony Hoare:
Message of thanks: on the receipt of the 2011 ACM SIGPLAN distinguished achievement award. 3-6
1.A: verification
- Stephan van Staden, Cristiano Calcagno, Bertrand Meyer:
Freefinement. 7-18 - Saurabh Joshi, Shuvendu K. Lahiri, Akash Lal:
Underspecified harnesses and interleaved bugs. 19-30 - Philippa Gardner, Sergio Maffeis
, Gareth David Smith:
Towards a program logic for JavaScript. 31-44
1.B: semantics
- Neelakantan R. Krishnaswami, Nick Benton, Jan Hoffmann:
Higher-order functional reactive programming in bounded space. 45-58 - Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis:
The marriage of bisimulations and Kripke logical relations. 59-72 - Roshan P. James, Amr Sabry:
Information effects. 73-84
2.A: privacy and access control
- Jean Yang, Kuat Yessenov, Armando Solar-Lezama:
A language for automatically enforcing privacy policies. 85-96 - Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella-Béguelin:
Probabilistic relational reasoning for differential privacy. 97-110 - Phillip Heidegger, Annette Bieniusa, Peter Thiemann:
Access permission contracts for scripting languages. 111-122
2.B: decision procedures
- Parthasarathy Madhusudan, Xiaokang Qiu, Andrei Stefanescu:
Recursive proofs for inductive tree data-structures. 123-136 - Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, Nikolaj S. Bjørner:
Symbolic finite state transducers: algorithms and applications. 137-150 - Ali Sinan Köksal, Viktor Kuncak, Philippe Suter:
Constraints as control. 151-164
3.A: security
- Thomas H. Austin, Cormac Flanagan:
Multiple facets for dynamic information flow. 165-178 - Donald Ray, Jay Ligatti:
Defining code-injection attacks. 179-190
3.B: complexity for concurrency
- Samik Basu, Tevfik Bultan, Meriem Ouederni:
Deciding choreography realizability. 191-202 - Ahmed Bouajjani, Michael Emmi:
Analysis of recursively parallel programs. 203-214
Invited talk
- Jennifer Rexford:
Programming languages for programmable networks. 215-216
4.A: medley
- Christopher Monsanto, Nate Foster, Rob Harrison, David Walker:
A compiler and run-time system for network programming languages. 217-230 - Ravi Chugh, Patrick Maxim Rondon, Ranjit Jhala:
Nested refinements: a logic for duck typing. 231-244 - Patrick Cousot, Radhia Cousot:
An abstract interpretation framework for termination. 245-258
4.B: mMechanized proofs
- Krystof Hoder, Laura Kovács, Andrei Voronkov:
Playing in the grey area of proofs. 259-272 - Antonis Stampoulis, Zhong Shao:
Static and user-extensible proof checking. 273-284 - Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, Robert Bruce Findler:
Run your research: on the effectiveness of lightweight mechanization. 285-296
5.A: concurrency
- Azadeh Farzan, Zachary Kincaid:
Verification of parameterized concurrent programs by modular reasoning about data and control. 297-308 - Matko Botincan, Mike Dodds, Suresh Jagannathan:
Resource-sensitive synchronization inference by abduction. 309-322 - Uday S. Reddy, John C. Reynolds:
Syntactic control of interference for separation logic. 323-336
5.B: type theory
- Daniel R. Licata, Robert Harper:
Canonicity for 2-dimensional type theory. 337-348 - Ohad Kammar, Gordon D. Plotkin:
Algebraic foundations for effect-dependent optimisations. 349-360 - Julien Cretin, Didier Rémy:
On the power of coercion abstraction. 361-372
6.A: dynamic analysis
- Mayur Naik, Hongseok Yang, Ghila Castelnuovo, Mooly Sagiv:
Abstractions from tests. 373-386 - Yannis Smaragdakis, Jacob Evans, Caitlin Sadowski, Jaeheon Yi, Cormac Flanagan:
Sound predictive race detection in polynomial time. 387-400
6.B: names and binders
- Mikolaj Bojanczyk, Laurent Braud, Bartek Klin, Slawomir Lasota:
Towards nominal computation. 401-412 - Andrew Cave, Brigitte Pientka:
Programming with binders and indexed data-types. 413-424
Invited talk 2
- J Strother Moore:
Meta-level features in an industrial-strength theorem prover. 425-426
7.A: verified transformations
- Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic:
Formalizing the LLVM intermediate representation for verified program transformations. 427-440 - Zeyuan Allen Zhu, Sasa Misailovic, Jonathan A. Kelner, Martin C. Rinard:
Randomized accuracy-aware program transformations for efficient approximate computations. 441-454 - Hongjin Liang, Xinyu Feng, Ming Fu:
A rely-guarantee-based simulation for verifying concurrent program transformations. 455-468
7.B: functional programming
- Thibaut Balabonski:
A unified approach to fully lazy sharing. 469-480 - Aseem Rastogi, Avik Chaudhuri, Basil Hosmer:
The ins and outs of gradual type inference. 481-494 - Martin Hofmann, Benjamin C. Pierce, Daniel Wagner:
Edit lenses. 495-508
8.A: C/C++ semantics
- Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, Peter Sewell:
Clarifying and compiling C/C++ concurrency: from C++11 to POWER. 509-520 - Tahina Ramananandro, Gabriel Dos Reis, Xavier Leroy:
A mechanized semantics for C++ object construction and destruction, with applications to resource management. 521-532 - Chucky Ellison, Grigore Rosu:
An executable formal semantics of C with applications. 533-544
8.B: type systems
- Sooraj Bhat, Ashish Agarwal, Richard W. Vuduc, Alexander G. Gray:
A type theory for probability density functions. 545-556 - Karl Naden, Robert Bocchino, Jonathan Aldrich, Kevin Bierhoff:
A type system for borrowing permissions. 557-570 - Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen:
Self-certification: bootstrapping certified typecheckers in F* with Coq. 571-584
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-12-12 23:04 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
