default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID43rd POPL 2016: St. Petersburg, FL, USA
- Rastislav Bodík, Rupak Majumdar:
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016. ACM 2016, ISBN 978-1-4503-3549-2
Keynotes
- Kathryn S. McKinley:
Programming the world of uncertain things (keynote). 1-2 - Richard M. Murray
:
Synthesis of reactive controllers for hybrid systems (keynote). 3 - David Walker:
Confluences in programming languages research (keynote). 4
Types and Foundations
- Matt Brown, Jens Palsberg:
Breaking through the normalization barrier: a self-interpreter for f-omega. 5-17 - Thorsten Altenkirch, Ambrus Kaposi:
Type theory in type theory using quotient inductive types. 18-29 - Yufei Cai, Paolo G. Giarrusso, Klaus Ostermann:
System f-omega with equirecursive types for datatype-generic programming. 30-43 - Pierre-Louis Curien, Marcelo P. Fiore, Guillaume Munch-Maccagnoni:
A theory of effects and resources: adjunction models and polarised calculi. 44-56
Algorithmic Verification
- Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno:
Temporal verification of higher-order functional programs. 57-68 - Gordon D. Plotkin, Nikolaj S. Bjørner, Nuno P. Lopes, Andrey Rybalchenko, George Varghese:
Scaling network verification using symmetry and surgery. 69-83 - James Brotherston, Nikos Gorogiannis, Max I. Kanovich, Reuben Rowe:
Model checking for symbolic-heap separation logic with inductive predicates. 84-96 - Eric Koskinen, Junfeng Yang:
Reducing crash recoverability to reachability. 97-108
Decision Procedures
- Xin Zhang, Ravi Mangal, Aditya V. Nori, Mayur Naik:
Query-guided maximum satisfiability. 109-122 - Anthony Widjaja Lin, Pablo Barceló:
String solving with word equations and transducers: towards a logic for analysing mutation XSS. 123-136 - Luca Cardelli, Mirco Tribastone, Max Tschaikowski, Andrea Vandin:
Symbolic computation of differential equivalences. 137-150 - Matthew Hague, Jonathan Kochems, C.-H. Luke Ong:
Unboundedness and downward closures of higher-order pushdown automata. 151-163
Correct Compilation
- Dominique Devriese, Marco Patrignani, Frank Piessens:
Fully-abstract compilation by approximate back-translation. 164-177 - Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis:
Lightweight verification of separate compilation. 178-190 - Edward Robbins, Andy King, Tom Schrijvers:
From MinX to MinC: semantics-driven decompilation of recursive datatypes. 191-203 - Florian Lorenzen, Sebastian Erdweg:
Sound type-dependent syntactic language extension. 204-216
Decidability and Complexity
- Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, Mooly Sagiv:
Decidability of inferring inductive invariants. 217-231 - Rahman Lavaee:
The hardness of data packing. 232-242 - Stéphane Gimenez, Georg Moser:
The complexity of interaction. 243-255
Language Design
- Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, Santiago Zanella-Béguelin:
Dependent types and multi-monadic effects in F. 256-270 - Johannes Borgström, Andrew D. Gordon, Long Ouyang, Claudio V. Russo, Adam Scibior, Marcin Szymczak:
Fabular: regression formulas as probabilistic programming. 271-283 - Niels Bjørn Bugge Grathwohl, Fritz Henglein, Ulrik Terp Rasmussen, Kristoffer Aalund Søholm, Sebastian Paaske Tørholm:
Kleenex: compiling nondeterministic transducers to deterministic streaming transducers. 284-297
Probabilistic and Statistical Analysis
- Fan Long, Martin C. Rinard:
Automatic patch generation by learning correct code. 298-312 - Omer Katz, Ran El-Yaniv, Eran Yahav:
Estimating types in binaries using predictive modeling. 313-326 - Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, Rouzbeh Hasheminezhad:
Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. 327-342 - Rishabh Singh, Sumit Gulwani:
Transforming spreadsheet data types using examples. 343-356
Foundations of Distributed Systems
- Mohsen Lesani, Christian J. Bell, Adam Chlipala:
Chapar: certified causally consistent distributed key-value stores. 357-370 - Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, Marc Shapiro:
'Cause I'm strong enough: reasoning about consistency choices in distributed systems. 371-384 - Hongjin Liang, Xinyu Feng:
A program logic for concurrent objects under fair scheduling. 385-399 - Cezara Dragoi, Thomas A. Henzinger, Damien Zufferey:
PSync: a partially synchronous language for fault-tolerant distributed algorithms. 400-415
Types, Generally or Gradually
- Sheng Chen, Martin Erwig:
Principal type inference for GADTs. 416-428 - Ronald Garcia, Alison M. Clark, Éric Tanter:
Abstracting gradual typing. 429-442 - Matteo Cimini, Jeremy G. Siek:
The gradualizer: a methodology and algorithm for generating gradual type systems. 443-455 - Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, Matthias Felleisen:
Is sound gradual typing dead? 456-468
Learning and Verification
- Damien Octeau, Somesh Jha, Matthew L. Dering, Patrick D. McDaniel, Alexandre Bartel, Li Li, Jacques Klein, Yves Le Traon:
Combining static analysis with probabilistic models to enable market-scale Android inter-component analysis. 469-484 - Radu Grigore, Hongseok Yang:
Abstraction refinement guided by a learnt probabilistic model. 485-498 - Pranav Garg, Daniel Neider, P. Madhusudan, Dan Roth:
Learning invariants using decision trees and implication counterexamples. 499-512 - Michael Emmi, Constantin Enea:
Symbolic abstract data type inference. 513-525
Optimization
- Somashekaracharya G. Bhaskaracharya, Uday Bondhugula, Albert Cohen:
SMO: an integrated approach to intra-array and inter-array storage optimization. 526-538 - Wenlei Bao, Sriram Krishnamoorthy, Louis-Noël Pouchet, Fabrice Rastello, P. Sadayappan:
PolyCheck: dynamic verification of iteration space transformations on affine programs. 539-554 - Marc Andrysco, Ranjit Jhala, Sorin Lerner:
Printing floating-point numbers: a faster, always correct method. 555-567
Sessions and Processes
- Dominic A. Orchard, Nobuko Yoshida:
Effects as sessions, sessions as effects. 568-581 - Limin Jia, Hannah Gommerstadt, Frank Pfenning:
Monitors and blame assignment for higher-order session types. 582-594 - Davide Sangiorgi, Valeria Vignudelli:
Environmental bisimulations for probabilistic higher-order languages. 595-607
Semantics and Memory Models
- Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, Peter Sewell:
Modelling the ARMv8 architecture, operationally: concurrency and ISA. 608-621 - Jean Pichon-Pharabod, Peter Sewell:
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. 622-633 - Mark Batty, Alastair F. Donaldson, John Wickerson:
Overhauling SC atomics in C11 and OpenCL. 634-648 - Ori Lahav, Nick Giannarakis, Viktor Vafeiadis:
Taming release-acquire consistency. 649-662
Program Design and Analysis
- Thomas W. Reps, Emma Turetsky, Prathmesh Prabhu:
Newtonian program analysis via tensor product. 663-677 - Rongxin Wu, Xiao Xiao, Shing-Chi Cheung, Hongyu Zhang, Charles Zhang:
Casper: an efficient approach to call trace collection. 678-690 - Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, David Van Horn:
Pushdown control-flow analysis for free. 691-704 - Matthew Flatt:
Binding as sets of scopes. 705-717
Foundations of Model Checking
- Ichiro Hasuo, Shunsuke Shimizu, Corina Cîrstea:
Lattice-theoretic progress measures and coalgebraic model checking. 718-732 - Krishnendu Chatterjee, Amir Kafshdar Goharshady, Rasmus Ibsen-Jensen, Andreas Pavlogiannis:
Algorithms for algebraic path properties in concurrent systems of constant treewidth components. 733-747 - Koko Muroya, Naohiko Hoshino, Ichiro Hasuo:
Memoryful geometry of interaction II: recursion and adequacy. 748-760
Synthesis
- Veselin Raychev, Pavol Bielik, Martin T. Vechev, Andreas Krause:
Learning programs from noisy data. 761-774 - James Bornholt, Emina Torlak, Dan Grossman, Luis Ceze:
Optimizing synthesis with metasketches. 775-788 - Aws Albarghouthi, Isil Dillig, Arie Gurfinkel:
Maximal specification synthesis. 789-801 - Jonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic:
Example-directed synthesis: a type-theoretic interpretation. 802-815
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-11-01 22:06 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:
