POPL 2014 logo

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.