POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages San Diego, USA January 22-24, 2014

Accepted papers

1. Sound Compilation of Reals.
   E. Darulova, V. Kuncak
2. Minimization of Symbolic Automata.
   L. D'Antoni, M. Veanes
3. Profiling For Laziness.
   S. Chang, M. Felleisen
4. Sound Input Filter Generation for Integer Overflow Errors.
   F. Long, S. Sidiroglou-Douskos, D. Kim, M. Rinard
5. Abstract Acceleration of General Linear Loops.
   B. Jeannet, P. Schrammel, S. Sankaranarayanan
6. Proofs that count.
   A. Farzan, Z. Kincaid, A. Podelski
7. Parametric Completeness for Separation Theories.
   J. Brotherston, J. Villard
8. FISSILE Type Analysis: Modular Checking of Almost Everywhere Invariants.
   D. Coughlin, B. Chang
9. Tabular: A Schema-Driven Probabilistic Programming Language.
   A. Gordon, T. Graepel, N. Rolland, C. Russo, J. Borgström, J. Guiver
10. Effect-Delimited Monad.
    S. Katsumata
11. Bias-Variance Tradeoffs in Program Analysis.
    A. Aiken, A. Nori, R. Sharma
12. Verifying Eventual Consistency of Optimistic Replication Systems.
    A. Bouajjani, C. Enea, J. Hamza
13. A Verified Information-Flow Architecture.
    A. de Amorim, N. Collins, A. DeHon, D. Demange, C. Hritcu, D. Pichardie, B. Pierce, R. Pollack, A. Tolmach
14. A non-standard standardization theorem.
    B. Accattoli, E. Bonelli, D. Kesner, C. Lombardi
15. On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs.
    M. Alberti, U. Dal Lago, D. Sangiorgi
16. Optimal Dynamic Partial Order Reduction.
    P. Abdulla, S. Aronis, B. Jonsson, K. Sagonas
17. Proof search for propositional abstract separation logics via labelled sequents.
    Z. Hou, R. Clouston, R. Gore, A. Tiu
18. Game semantics for Interface Middleweight Java.
    A. Murawski, N. Tzevelekos
19. A Sound and Complete Abstraction for Reasoning About Parallel Prefix Sums.
    N. Chong, A. Donaldson, J. Ketema
20. Abstract Effects and Proof-Relevant Logical Relations.
    N. Benton, M. Hofmann, V. Nigam
21. Closed type families with overlapping equations.
    R. Eisenberg, D. Vytiniotis, S. Peyton Jones, S. Weirich
22. Combining Proofs and Programs in a Dependently Typed Language.
    C. Casinghino, V. Sjoeberg, S. Weirich
23. Consistency Analysis of Decision-Making Programs.
    S. Chaudhuri, A. Farzan, Z. Kincaid
24. Toward General Diagnosis of Static Errors.
    D. Zhang, A. Myers
25. Probabilistic Relational Verification for Cryptographic Implementations.
    G. Barthe, C. Fournet, B. Grégoire, P. Strub, N. Swamy, S. Zanella-Béguelin
26. A Proof System for Separation Logic with Magic Wand.
    W. Lee, S. Park
27. An Abstraction Refinement Approach to Higher-Order Model Checking.
    S. Ramsay, R. Neatherway, L. Ong
28. Gradual Typing Embedded Securely in JavaScript.
    K. Bhargavan, G. Bierman, J. Chen, C. Fournet, A. Rastogi, P. Strub, N. Swamy
29. Fair Reactive Programming.
    A. Cave, F. Ferreira, P. Panangaden, B. Pientka
30. Freeze After Writing: Quasi-Deterministic Parallel Programming with LVars and Callbacks.
    L. Kuper, A. Turon, N. Krishnaswami, R. Newton
31. Authenticated Data Structures, Generically.
    A. Miller, M. Hicks, J. Katz, E. Shi
32. Backpack: Retrofitting Haskell with Interfaces.
    S. Kilpatrick, D. Dreyer, S. Peyton Jones, S. Marlow
33. Symbolic Optimization with SMT Solvers.
    Y. Li, A. Albarghouthi, Z. Kincaid, A. Gurfinkel, M. Chechik
34. Applying quantitative semantics to higher-order quantum computing.
    M. Pagani, P. Selinger, B. Valiron
35. Replicated Data Types: Specification, Verification, Optimality.
    S. Burckhardt, A. Gotsman, H. Yang, M. Zawirski
36. NetKAT: Semantic Foundations for Networks.
    C. Anderson, N. Foster, A. Guha, J. Jeannin, D. Kozen, C. Schlesinger, D. Walker
37. Abstract Satisfaction.
    V. D'Silva, L. Haller, D. Kroening
38. Battery Transition Systems.
    U. Boker, T. Henzinger, A. Radhakrishna
39. Bridging Boolean and Quantitative Synthesis Using Smoothed Proof Search.
    M. Clochard, S. Chaudhuri, A. Solar-Lezama
40. CakeML: A Verified Implementation of ML.
    R. Kumar, M. Myreen, S. Owens, M. Norrish
41. From Parametricity to Conservation Laws, via Noether's Theorem.
    R. Atkey
42. Polymorphic Functions with Set-Theoretic Types (Part 1: Syntax, Semantics, and Evaluation).
    G. Castagna, K. Nguyễn, Z. Xu, H. Im, S. Lenglet, L. Padovani
43. A Constraint-Based Approach to Solving Games on Infinite Graphs.
    T. Beyene, S. Chaudhuri, C. Popeea, A. Rybalchenko
44. Tracing Compilation by Abstract Interpretation.
    S. Dissegna, F. Logozzo, F. Ranzato
45. Counter-Factual Typing for Debugging Type Errors.
    S. Chen, M. Erwig
46. Modular, Higher-Order Cardinality Analysis in Theory and Practice.
    I. Sergey, D. Vytiniotis, S. Peyton Jones
47. Modular Reasoning on Unique Heap Paths via Effectively Propositional Formulas.
    S. Itzhaky, O. Lahav, A. Banerjee, N. Immerman, A. Nanevski, M. Sagiv
48. Probabilistic Coherence Spaces are Fully Abstract for Probabilistic PCF.
    T. Ehrhard, M. Pagani, C. Tasson
49. A Relationally Parametric Model of Dependent Type Theory.
    R. Atkey, N. Ghani, P. Johann
50. A Trusted Mechanised JavaScript Specification.
    M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, G. Smith
51. An operational and axiomatic semantics for non-determinism and sequence points in C.
    R. Krebbers

In total 51 papers were accepted out of 220 submissions.