


default search action
42nd POPL 2015: Mumbai, India
- Sriram K. Rajamani, David Walker

:
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. ACM 2015, ISBN 978-1-4503-3300-9
Keynote Address
- Sumit Gulwani:

Automating Repetitive Tasks for the Masses. 1-2
Session 1A: Types I
- Paul-André Melliès

, Noam Zeilberger
:
Functors are Type Refinement Systems. 3-16 - Neelakantan R. Krishnaswami, Cécilia Pradic, Nick Benton:

Integrating Linear and Dependent Types. 17-30 - Kristina Sojakova:

Higher Inductive Types as Homotopy-Initial Algebras. 31-42
Session 1B: Security
- Minh Ngo

, Fabio Massacci
, Dimiter Milushev, Frank Piessens:
Runtime Enforcement of Security Policies on Black Box Reactive Programs. 43-54 - Gilles Barthe

, Marco Gaboardi
, Emilio Jesús Gallego Arias, Justin Hsu
, Aaron Roth
, Pierre-Yves Strub:
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. 55-68 - Hamid Ebadi, David Sands, Gerardo Schneider:

Differential Privacy: Now it's Getting Personal. 69-81
Session 2A: Program Analysis I
- Hao Tang, Xiaoyin Wang

, Lingming Zhang, Bing Xie, Lu Zhang, Hong Mei:
Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks. 83-95 - Krishnendu Chatterjee, Rasmus Ibsen-Jensen

, Andreas Pavlogiannis
, Prateesh Goyal:
Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth. 97-109 - Veselin Raychev, Martin T. Vechev, Andreas Krause:

Predicting Program Properties from "Big Code". 111-124
Session 2B: Domain-specific Languages
- Rajeev Alur, Loris D'Antoni, Mukund Raghothaman

:
DReX: A Declarative Language for Efficiently Evaluating Regular String Transformations. 125-137 - Margus Veanes, Todd Mytkowicz, David Molnar, Benjamin Livshits:

Data-Parallel String-Manipulating Programs. 139-152 - Adam Chlipala:

Ur/Web: A Simple Model for Programming the Web. 153-165
Session 3A: Dynamic Verification
- Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin M. Bierman, Panagiotis Vekris:

Safe & Efficient Gradual Typing for TypeScript. 167-180 - Michael Greenberg

:
Space-Efficient Manifest Contracts. 181-194 - Taro Sekiyama, Yuki Nishida

, Atsushi Igarashi:
Manifest Contracts for Datatypes. 195-207
Session 3B: Concurrency I
- Viktor Vafeiadis

, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli:
Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it. 209-220 - Julien Lange

, Emilio Tuosto, Nobuko Yoshida
:
From Communicating Machines to Graphical Choreographies. 221-232 - Mike Dodds

, Andreas Haas, Christoph M. Kirsch:
A Scalable, Correct Time-Stamped Stack. 233-246
Session 4A: Compiler Correctness
- Jacques-Henri Jourdan

, Vincent Laporte, Sandrine Blazy
, Xavier Leroy, David Pichardie:
A Formally-Verified C Static Analyzer. 247-259 - Roberto Giacobazzi, Francesco Logozzo, Francesco Ranzato:

Analyzing Program Analyses. 261-273 - Gordon Stewart, Lennart Beringer, Santiago Cuéllar, Andrew W. Appel

:
Compositional CompCert. 275-287
Session 4B: Types II
- Giuseppe Castagna

, Kim Nguyen, Zhiwu Xu, Pietro Abate:
Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction. 289-302 - Ronald Garcia, Matteo Cimini:

Principal Type Schemes for Gradual Programs. 303-315 - Luísa Lourenço, Luís Caires:

Dependent Information Flow Types. 317-328
Session 5A: Regular Languages and Automata
- Mila Dalla Preda, Roberto Giacobazzi, Arun Lakhotia, Isabella Mastroeni

:
Abstract Symbolic Automata: Mixed syntactic/semantic similarity analysis of executables. 329-341 - Nate Foster, Dexter Kozen, Mae Milano

, Alexandra Silva, Laure Thompson
:
A Coalgebraic Decision Procedure for NetKAT. 343-355 - Damien Pous

:
Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests. 357-368
Session 5B: Programming Models I
- Vilhelm Sjöberg, Stephanie Weirich

:
Programming up to Congruence. 369-382 - Kazunori Tobisawa:

A Meta Lambda Calculus with Cross-Level Computation. 383-393 - Sam Staton:

Algebraic Effects, Linearity, and Quantum Programming Languages. 395-406
Session 6A: Concurrency II
- Azadeh Farzan, Zachary Kincaid

, Andreas Podelski:
Proof Spaces for Unbounded Parallelism. 407-420 - Davide Sangiorgi:

Equations, Contractions, and Unique Solutions. 421-432 - Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakrishna

, Roopsha Samanta, Thorsten Tarrach:
Succinct Representation of Concurrent Trace Sets. 433-444
Session 6B: Semantics
- Denis Bogdanas, Grigore Rosu:

K-Java: A Complete Semantics of Java. 445-456 - Michael D. Adams:

Towards the Essence of Hygiene. 457-469 - Matt Brown, Jens Palsberg:

Self-Representation in Girard's System U. 471-484
Keynote Address
- Peter Lee:

Coding by Everyone, Every Day. 485 - Peter Buneman:

Databases and Programming: Two Subjects Divided by a Common Language? 487
Session 7A: Probabilistic Programs
- Luis María Ferrer Fioriti, Holger Hermanns

:
Probabilistic Termination: Soundness, Completeness, and Compositionality. 489-501 - Fei He, Xiaowei Gao, Bow-Yaw Wang, Lijun Zhang:

Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems. 503-514
Session 7B: Programming Models II
- Filippo Bonchi

, Pawel Sobocinski
, Fabio Zanasi
:
Full Abstraction for Signal Flow Graphs. 515-526 - Ralf Hinze, Nicolas Wu

, Jeremy Gibbons:
Conjugate Hylomorphisms - Or: The Mother of All Structured Recursion Schemes. 527-538
Session 8A: Program Analysis II
- Krishnendu Chatterjee, Andreas Pavlogiannis

, Yaron Velner:
Quantitative Interprocedural Analysis. 539-551 - Osbert Bastani, Saswat Anand, Alex Aiken

:
Specification Inference Using Context-Free Language Reachability. 553-566 - Venmugil Elango, Fabrice Rastello, Louis-Noël Pouchet, J. Ramanujam

, P. Sadayappan
:
On Characterizing the Data Access Complexity of Programs. 567-580
Session 8B: Verification
- Pieter Agten, Bart Jacobs

, Frank Piessens:
Sound Modular Verification of C Code Executing in an Unverified Context. 581-594 - Ronghui Gu, Jérémie Koenig

, Tahina Ramananandro
, Zhong Shao
, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, Yu Guo:
Deep Specifications and Certified Abstraction Layers. 595-608 - Adam Chlipala:

From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification. 609-622
Session 9A: Concurrency III
- Karl Crary, Michael J. Sullivan

:
A Calculus for Relaxed Memory. 623-636 - Ralf Jung

, David Swasey
, Filip Sieczkowski
, Kasper Svendsen, Aaron Turon, Lars Birkedal
, Derek Dreyer:
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. 637-650 - Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza:

Tractable Refinement Checking for Concurrent Objects. 651-662
Session 9B: Synthesis
- Oded Padon

, Neil Immerman, Aleksandr Karbyshev
, Ori Lahav
, Mooly Sagiv, Sharon Shoham
:
Decentralizing SDN Policies. 663-676 - Robert A. Cochran, Loris D'Antoni, Benjamin Livshits, David Molnar, Margus Veanes:

Program Boosting: Program Synthesis via Crowd-Sourcing. 677-688 - Benjamin Delaware, Clément Pit-Claudel

, Jason Gross, Adam Chlipala:
Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. 689-700

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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














