![](https://dblp.dagstuhl.de/img/logo.ua.320x120.png)
![](https://dblp.dagstuhl.de/img/dropdown.dark.16x16.png)
![](https://dblp.dagstuhl.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
![search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
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 Cuellar, 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
![](https://dblp.dagstuhl.de/img/cog.dark.24x24.png)
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.