gasche/popl2014-papers

POPL is the symposium on Principles of Programming Languages. The 2014 edition will take place in San Diego, from January 22 to January 24.

The list of accepted papers was published there. The present page tries to gather preprint links and complementary information; please do not hesitate to submit issues or pull requests. Patch authors: please pay attention to the two non-erasable whitespaces required to add a line break after each link.

(See here for a similar page for ICFP'13)

Edit

As of late January 2014, the official POPL proceedings are publicly available for download from the POPL website. This is a truly excellent initiative. We can only hope they will remain available in the future, and similar miracles will happen for the next editions of this conference. Thanks!

POPL-2014

• Sound Compilation of Reals. 
  (preprint) (arxiv),
  E. Darulova, V. Kuncak

• Minimization of Symbolic Automata. 
  (preprint) (technical report) (webpage),
  L. D'Antoni, M. Veanes

• Profiling For Laziness. 
  (preprint),
  S. Chang, M. Felleisen

• Sound Input Filter Generation for Integer Overflow Errors. 
  (technical report) (website),
  F. Long, S. Sidiroglou-Douskos, D. Kim, M. Rinard

• Abstract Acceleration of General Linear Loops. 
  (arxiv),
  B. Jeannet, P. Schrammel, S. Sankaranarayanan

• Proofs that count. 
  (preprint),
  A. Farzan, Z. Kincaid, A. Podelski

• Parametric Completeness for Separation Theories. 
  (preprint) (slides),
  J. Brotherston, J. Villard

• FISSILE Type Analysis: Modular Checking of Almost Everywhere Invariants. 
  (no preprint found),
  D. Coughlin, B. Chang

• Tabular: A Schema-Driven Probabilistic Programming Language. 
  (no preprint found),
  A. Gordon, T. Graepel, N. Rolland, C. Russo, J. Borgström, J. Guiver

• Effect-Delimited Monad. 
  (no preprint found),
  S. Katsumata

• Bias-Variance Tradeoffs in Program Analysis. 
  (preprint),
  A. Aiken, A. Nori, R. Sharma

• Verifying Eventual Consistency of Optimistic Replication Systems. 
  (preprint) (previous related work),
  A. Bouajjani, C. Enea, J. Hamza

• A Verified Information-Flow Architecture. 
  (draft),
  A. Azevedo de Amorim, N. Collins, A. DeHon, D. Demange, C. Hriţcu, D. Pichardie, B. Pierce, R. Pollack, A. Tolmach

• A non-standard standardization theorem. 
  (preprint)
  B. Accattoli, E. Bonelli, D. Kesner, C. Lombardi

• On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs. 
  (arxiv),
  M. Alberti, U. Dal Lago, D. Sangiorgi

• Optimal Dynamic Partial Order Reduction. 
  (preprint),
  P. Abdulla, S. Aronis, B. Jonsson, K. Sagonas

• Proof search for propositional abstract separation logics via labelled sequents. 
  (arxiv),
  Z. Hou, R. Clouston, R. Gore, A. Tiu

• Game semantics for Interface Middleweight Java. 
  (no preprint found) (previous related work),
  A. Murawski, N. Tzevelekos

• A Sound and Complete Abstraction for Reasoning About Parallel Prefix Sums. 
  (preprint),
  N. Chong, A. Donaldson, J. Ketema

• Abstract Effects and Proof-Relevant Logical Relations. 
  (arxiv),
  N. Benton, M. Hofmann, V. Nigam

• Closed type families with overlapping equations. 
  (preprint) (extended version),
  R. Eisenberg, D. Vytiniotis, S. Peyton Jones, S. Weirich

• Combining Proofs and Programs in a Dependently Typed Language. 
  (preprint),
  C. Casinghino, V. Sjöberg, S. Weirich

• Consistency Analysis of Decision-Making Programs. 
  (preprint),
  S. Chaudhuri, A. Farzan, Z. Kincaid

• Toward General Diagnosis of Static Errors. 
  (technical report),
  D. Zhang, A. Myers

• Probabilistic Relational Verification for Cryptographic Implementations. 
  (draft),
  G. Barthe, C. Fournet, B. Grégoire, P. Strub, N. Swamy, S. Zanella-Béguelin

• A Proof System for Separation Logic with Magic Wand. 
  (technical report) (website),
  Wonyel Lee, Sungwoo Park

• An Abstraction Refinement Approach to Higher-Order Model Checking. 
  (draft),
  Steven Ramsay, Robin Neatherway, Luke Ong

• Gradual Typing Embedded Securely in JavaScript. 
  (draft),
  K. Bhargavan, G. Bierman, J. Chen, C. Fournet, A. Rastogi, P. Strub, N. Swamy

• Fair Reactive Programming. 
  (preprint) (long version),
  A. Cave, F. Ferreira, P. Panangaden, B. Pientka

• Freeze After Writing: Quasi-Deterministic Parallel Programming with LVars. 
  (preprint) (github),
  L. Kuper, A. Turon, N. Krishnaswami, R. Newton

• Authenticated Data Structures, Generically. 
  (preprint), (github)
  A. Miller, M. Hicks, J. Katz, E. Shi

• Backpack: Retrofitting Haskell with Interfaces. 
  (preprint) (website),
  S. Kilpatrick, D. Dreyer, S. Peyton Jones, S. Marlow

• Symbolic Optimization with SMT Solvers. 
  (preprint),
  Y. Li, A. Albarghouthi, Z. Kincaid, A. Gurfinkel, M. Chechik

• Applying quantitative semantics to higher-order quantum computing. 
  (arxiv),
  M. Pagani, P. Selinger, B. Valiron

• Replicated Data Types: Specification, Verification, Optimality.
  (webpage) (preprint),
  S. Burckhardt, A. Gotsman, H. Yang, M. Zawirski

• NetKAT: Semantic Foundations for Networks. 
  (preprint),
  C. Anderson, N. Foster, A. Guha, J. Jeannin, D. Kozen, C. Schlesinger, D. Walker

• Abstract Satisfaction. 
  V. D'Silva, L. Haller, D. Kröning

• Battery Transition Systems. 
  U. Boker, T. Henzinger, A. Radhakrishna

• Bridging Boolean and Quantitative Synthesis Using Smoothed Proof Search. 
  (preprint),
  M. Clochard, S. Chaudhuri, A. Solar-Lezama

• CakeML: A Verified Implementation of ML. 
  (preprint),
  R. Kumar, M. Myreen, S. Owens, M. Norrish

• From Parametricity to Conservation Laws, via Noether's Theorem. 
  (preprint) (webpage),
  R. Atkey

• Polymorphic Functions with Set-Theoretic Types (Part 1: Syntax, Semantics, and Evaluation). 
  (preprint)
  G. Castagna, K. Nguyễn, Z. Xu, H. Im, S. Lenglet, L. Padovani

• A Constraint-Based Approach to Solving Games on Infinite Graphs. 
  (preprint),
  T. Beyene, S. Chaudhuri, C. Popeea, A. Rybalchenko

• Tracing Compilation by Abstract Interpretation. 
  (preprint),
  S. Dissegna, F. Logozzo, F. Ranzato

• Counter-Factual Typing for Debugging Type Errors. 
  (preprint),
  S. Chen, M. Erwig

• Modular, Higher-Order Cardinality Analysis in Theory and Practice. 
  (extended version),
  I. Sergey, D. Vytiniotis, S. Peyton Jones

• Modular Reasoning on Unique Heap Paths via Effectively Propositional Formulas. 
  S. Itzhaky, O. Lahav, A. Banerjee, N. Immerman, A. Nanevski, M. Sagiv

• Probabilistic Coherence Spaces are Fully Abstract for Probabilistic PCF. 
  T. Ehrhard, M. Pagani, C. Tasson

• A Relationally Parametric Model of Dependent Type Theory. 
  (preprint) (webpage),
  R. Atkey, N. Ghani, P. Johann

• A Trusted Mechanised JavaScript Specification. 
  (preprint),
  M. Bodin, A. Charguéraud, D. Filaretti, P. Gardner, S. Maffeis, D. Naudziuniene, A. Schmitt, G. Smith

• An operational and axiomatic semantics for non-determinism and sequence points in C. 
  (preprint) (Coq source),
  R. Krebbers

Affiliated events

(Feel free to send me pull request with the programme of the affiliated events, even if you don't have much preprint links, when they become available.)

PADL-2014

The list of accepted papers is available here.

• Two Applications of the ASP-Prolog System: Decomposable Programs and Multi-context Systems.
  (no preprint found)
  Tran Cao Son, Enrico Pontelli, Tiep Le

• Partial Type Signatures for Haskell.
  (extended version)
  Thomas Winant, Dominique Devriese, Frank Piessens, Tom Schrijvers

• Towards Modeling Morality Computationally with Logic Programming.
  (preprint)
  Ari Saptawijaya, Luís Moniz Pereira

• Abstract Modular Inference Systems and Solvers.
  (preprint)
  Yuliya Lierler, Mirek Truszczynski

• Compiling DNA strand displacement reactions using a functional programming language.
  (preprint)
  Matthew R. Lakin, Andrew Phillips

• Sunroof: A Monadic DSL for Generating JavaScript.
  (preprint)
  Andy Gill, Jan Bracker

• Exploring the Use of GPUs in Constraint Solving.
  Federico Campeotto, Alessandro Dal Palù, Agostino Dovier, Ferdinando Fioretto, Enrico Pontelli

• On the Correctness and Efficiency of Lock-Free Expandable Tries for Tabled Logic Programs.
  (preprint) Miguel Areias, Ricardo Rocha

• The F# Computation Expressions Zoo.
  (preprint)
  Tomas Petricek, Don Syme

• Embedding Foreign Code.
  (preprint)
  Robert Clifton-Everest, Trevor L. McDonell, Manuel Chakravarty, Gabriele Keller

• Typelets - A Rule-Based Evaluation Model for Dynamic, Statically Typed User Interfaces.
  (preprint)
  Martin Elsman, Anders Schack-Nielsen

• Rx-CML: A Prescription for Safely Relaxing Synchrony.
  (preprint)
  KC Sivaramakrishnan, Lukasz Ziarek, Suresh Jagannathan

• Panext: Towards an extendible Pandoc system.
  Jacco O.G. Krijnen, Doaitse Swierstra, Marcos O. Viera

• A Declarative Specification of Giant Number Arithmetic.
  (arxiv)
  Paul Tarau

• Generic Generic Programming.
  (preprint
  José Pedro Magalhães, Andres Löh

PEPM-2014

• Semantic Bidirectionalization Revisited. 
  (no preprint found)
  Meng Wang, Shayan Najd

• Optimizing SYB is Easy!. 
  (preprint)
  (preprint)
  Michael D. Adams, Andrew Farmer, José Pedro Magalhães

• Early Detection of Type Errors in C++ Templates. 
  (preprint)
  Sheng Chen, Martin Erwig

• An Operational Semantics for Android Activities. 
  (no preprint found)
  Étienne Payet, Fausto Spoto

• QEMU/CPC: Static Analysis and CPS Conversion for Safe, Portable, and Efficient Coroutines. 
  (arxiv)
  Gabriel Kerneis, Charlie Shepherd, Stefan Hajnoczi

• Type-Changing Rewriting and Semantics-Preserving Transformation. 
  (technical report)
  Sean Leather, Johan Jeuring, Andres Löh, Bram Schuur

• Lazy Stateless Incremental Evaluation Machinery for Attribute Grammars. 
  (preprint)
  Jeroen Bransen, Atze Dijkstra, Doaitse Swierstra

• The HERMIT in the Stream. 
  (preprint)
  Andrew Farmer, Christian Hoener zu Siederdissen, Andy Gill

• Monadic Combinators for "Putback" Style Bidirectional Programming. 
  (preprint)
  Hugo Pacheco, Zhenjiang Hu, Sebastian Fischer

• Effective Quotation. 
  (arxiv)
  James Cheney, Sam Lindley, Gabriel Radanne, Philip Wadler

• Compile-time Reflection and Metaprogramming for Java. 
  (preprint)
  Weiyu Miao, Jeremy Siek

• Combinators for Impure yet Hygienic Code Generation. 
  (no preprint found)
  Yukiyoshi Kameyama, Oleg Kiselyov, Chung-Chieh Shan

• Automating Property-based Testing of Evolving Web Services. 
  (preprint)
  Huiqing Li, Simon Thompson, Pablo Lamela Seijas, Miguel Angel Francisco

• Deriving Interpretations of the Gradually-Typed Lambda Calculus. 
  (preprint),
  Álvaro Garca-Prez, Pablo Nogueira, Ilya Sergey

• HIPimm: Verifying Granular Immutability Guarantees. 
  (preprint)
  Andreea Costea, Asankhaya Sharma, Cristina David

• A Modular and Generic Analysis Server System for Functional Logic Programs. 
  (no preprint found) (similar),
  Michael Hanus, Fabian Skrlac

• Generating attribute grammar-based bidirectional transformations from rewrite-rules. 
  (preprint)
  Pedro Martins, João Paulo Fernandes, João Saraiva, Eric Van Wyk

PLPV-2014

• Programming Languages for High-Assurance Autonomous Vehicles. 
  (no preprint found)
  Lee Pike

• The Recursive Polarized Dual Calculus. 
  (preprint)
  Aaron Stump

• Substructural Typestates. 
  (preprint)
  Filipe Militao, Jonathan Aldrich, Luis Caires

• Refinement Types For Haskell. 
  (no preprint found)
  Ranjit Jhala

• Verified Programs with Binders. 
  (preprint)
  Martin Clochard, Claude Marché, Andrei Paskevich

• Formalizing a Correctness Property of a Type-Directed Partial Evaluator. 
  (no preprint found)
  Noriko Hirota, Kenichi Asai

• An Abstract Categorical Semantics for Functional Reactive Programming with Processes. 
  (no preprint found)
  Wolfgang Jeltsch

VMCAI-2014

• Practical Floating-Point Tests with Integer Code. 
  (no preprint found)
  Anthony Romano

• Weakest Precondition Synthesis for Compiler Optimizations. 
  (abstract) (no preprint found),
  Nuno P. Lopes, José Monteiro

• Precise analysis of value-dependent synchronization in programs with priority scheduling. 
  (no preprint found)
  Martin Schwarz, Helmut Seidl, Vesal Vojdani, Kalmer Apinis

• Deciding Control State Reachability in Concurrent Traces with Limited Observability. 
  (preprint)
  Chao Wang, Kevin Hoang

• Monitoring Parametric Temporal Logic. 
  (no preprint found)
  Peter Faymonville, Bernd Finkbeiner, Doron Peled

• SAT-Based Synthesis Methods for Safety Specs. 
  (arxiv)
  Roderick Bloem, Robert Könighofer, Martina Seidl

• Bisimulations and Logical Characterizations on Continuous-time Markov Decision Processes. 
  (no preprint found)
  Lei Song, Lijun Zhang, Jens Chr. Godskesen

• Doomsday Equilibria for Omega-Regular Games. 
  (arxiv)
  Krishnendu Chatterjee, Laurent Doyen, Emmanuel Filiot, Jean-Francois Raskin

• Policy Iteration-based Conditional Termination and Ranking Functions. 
  (preprint)
  Damien Massé

• Timing Analysis of Parallel Software Using Abstract Execution. 
  (no preprint found)
  Andreas Gustavsson, Jan Gustafsson, Björn Lisper

• Parameterized Model Checking of Token-Passing Systems. 
  (arxiv)
  Benjamin Aminof, Swen Jacobs, Ayrat Khalimov, Sasha Rubin

• Generic Combination of Heap and Value Analysis in Abstract Interpretation. 
  (no preprint found)
  Pietro Ferrara

• Verifying Array Programs by Transforming Verification Conditions. 
  (preprint)
  Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti

• A Logic-based Framework for Verifying Consensus Algorithms. 
  (preprint)
  Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, Damien Zufferey

• Relational Thread-Modular Static Value Analysis by Abstract Interpretation. 
  (preprint)
  Antoine Miné

• Modular Synthesis of Sketches using Models. 
  (preprint)
  Rohit Singh, Rishabh Singh, Zhilei Xu, Rebecca Krosnick, Armando Solar-Lezama

• Widening for Control-Flow. 
  (preprint)
  Ben Hardekopf, Ben Wiedermann, Berkeley Churchill, Vineeth Kashyap

• Synthesis with Identifiers. 
  (preprint)
  Rüdiger Ehlers, Sanjit A. Seshia, Hadas Kress-Gazit

• Synthesis for Polynomial Lasso Programs. 
  (arxiv)
  Jan Leike, Ashish Tiwari

• Probabilistic Automata for Safety LTL Specifications. 
  (no preprint found)
  Dileep Kini, Mahesh Viswanathan

• Safety Problems are NP-complete for Flat Integer Programs with Octagonal Loops. 
  (arxiv)
  Radu Iosif, Marius Bozga, Filip Konecny

• Modelling parsimonious putative regulatory networks: complexity and heuristic approaches. 
  (no preprint found)
  Vicente Acuña, Andres Aravena, Alejandro Maass, Anne Siegel

• Message Passing Algorithms for the Verification of Distributed Protocols. 
  (preprint)
  Loig Jezequel, Javier Esparza

• Modularly Combining Numeric Abstract Domains with Points-to Analysis, and a Scalable Static Numeric Analyzer for Java. 
  (preprint)
  Zhoulai Fu

• Cascade 2.0 (Tool Paper). 
  (preprint)
  Wei Wang, Clark Barrett, Thomas Wies