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
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
Runtime Enforcement of Security Policies on Black Box Reactive Programs. 43-54 - Gilles Barthe
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
Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks. 83-95 - Krishnendu Chatterjee, Rasmus Ibsen-Jensen
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
Manifest Contracts for Datatypes. 195-207
Session 3B: Concurrency I
- Viktor Vafeiadis
Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it. 209-220 - Julien Lange
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
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
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
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
Proof Spaces for Unbounded Parallelism. 407-420 - Davide Sangiorgi:
Equations, Contractions, and Unique Solutions. 421-432 - Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakrishna
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
Full Abstraction for Signal Flow Graphs. 515-526 - Ralf Hinze, Nicolas Wu
Conjugate Hylomorphisms - Or: The Mother of All Structured Recursion Schemes. 527-538
Session 8A: Program Analysis II
- Krishnendu Chatterjee, Andreas Pavlogiannis
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
On Characterizing the Data Access Complexity of Programs. 567-580
Session 8B: Verification
- Pieter Agten, Bart Jacobs
Sound Modular Verification of C Code Executing in an Unverified Context. 581-594 - Ronghui Gu, Jérémie Koenig
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
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
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
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.
last updated on 2024-12-19 22:00 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: