| 2014 | 30 years of research and development around Coq. Gérard P. Huet, Hugo Herbelin |
| 2014 | A Galois connection calculus for abstract interpretation. Patrick Cousot, Radhia Cousot |
| 2014 | A constraint-based approach to solving games on infinite graphs. Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, Andrey Rybalchenko |
| 2014 | A nonstandard standardization theorem. Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, Carlos Lombardi |
| 2014 | A proof system for separation logic with magic wand. Wonyeol Lee, Sungwoo Park |
| 2014 | A relationally parametric model of dependent type theory. Robert Atkey, Neil Ghani, Patricia Johann |
| 2014 | A sound and complete abstraction for reasoning about parallel prefix sums. Nathan Chong, Alastair F. Donaldson, Jeroen Ketema |
| 2014 | A trusted mechanised JavaScript specification. Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, Gareth Smith |
| 2014 | A type-directed abstraction refinement approach to higher-order model checking. Steven J. Ramsay, Robin P. Neatherway, C.-H. Luke Ong |
| 2014 | A verified information-flow architecture. Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach |
| 2014 | Abstract acceleration of general linear loops. Bertrand Jeannet, Peter Schrammel, Sriram Sankaranarayanan |
| 2014 | Abstract effects and proof-relevant logical relations. Nick Benton, Martin Hofmann, Vivek Nigam |
| 2014 | Abstract satisfaction. Vijay Victor D'Silva, Leopold Haller, Daniel Kroening |
| 2014 | An operational and axiomatic semantics for non-determinism and sequence points in C. Robbert Krebbers |
| 2014 | Applying quantitative semantics to higher-order quantum computing. Michele Pagani, Peter Selinger, Benoît Valiron |
| 2014 | Authenticated data structures, generically. Andrew Miller, Michael Hicks, Jonathan Katz, Elaine Shi |
| 2014 | Backpack: retrofitting Haskell with interfaces. Scott Kilpatrick, Derek Dreyer, Simon L. Peyton Jones, Simon Marlow |
| 2014 | Battery transition systems. Udi Boker, Thomas A. Henzinger, Arjun Radhakrishna |
| 2014 | Bias-variance tradeoffs in program analysis. Rahul Sharma, Aditya V. Nori, Alex Aiken |
| 2014 | Bridging boolean and quantitative synthesis using smoothed proof search. Swarat Chaudhuri, Martin Clochard, Armando Solar-Lezama |
| 2014 | CakeML: a verified implementation of ML. Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens |
| 2014 | Closed type families with overlapping equations. Richard A. Eisenberg, Dimitrios Vytiniotis, Simon L. Peyton Jones, Stephanie Weirich |
| 2014 | Combining proofs and programs in a dependently typed language. Chris Casinghino, Vilhelm Sjöberg, Stephanie Weirich |
| 2014 | Consistency analysis of decision-making programs. Swarat Chaudhuri, Azadeh Farzan, Zachary Kincaid |
| 2014 | Counter-factual typing for debugging type errors. Sheng Chen, Martin Erwig |
| 2014 | Fair reactive programming. Andrew Cave, Francisco Ferreira, Prakash Panangaden, Brigitte Pientka |
| 2014 | Fissile type analysis: modular checking of almost everywhere invariants. Devin Coughlin, Bor-Yuh Evan Chang |
| 2014 | Freeze after writing: quasi-deterministic parallel programming with LVars. Lindsey Kuper, Aaron Turon, Neelakantan R. Krishnaswami, Ryan R. Newton |
| 2014 | From parametricity to conservation laws, via Noether's theorem. Robert Atkey |
| 2014 | Game semantics for interface middleweight Java. Andrzej S. Murawski, Nikos Tzevelekos |
| 2014 | Gradual typing embedded securely in JavaScript. Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman |
| 2014 | Minimization of symbolic automata. Loris D'Antoni, Margus Veanes |
| 2014 | Modular reasoning about concurrent higher-order imperative programs. Lars Birkedal |
| 2014 | Modular reasoning about heap paths via effectively propositional formulas. Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv |
| 2014 | Modular, higher-order cardinality analysis in theory and practice. Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones |
| 2014 | NetkAT: semantic foundations for networks. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, David Walker |
| 2014 | On coinductive equivalences for higher-order probabilistic functional programs. Ugo Dal Lago, Davide Sangiorgi, Michele Alberti |
| 2014 | Optimal dynamic partial order reduction. Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, Konstantinos Sagonas |
| 2014 | Parametric completeness for separation theories. James Brotherston, Jules Villard |
| 2014 | Parametric effect monads and semantics of effect systems. Shin-ya Katsumata |
| 2014 | Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation. Giuseppe Castagna, Kim Nguyen, Zhiwu Xu, Hyeonseung Im, Sergueï Lenglet, Luca Padovani |
| 2014 | Probabilistic coherence spaces are fully abstract for probabilistic PCF. Thomas Ehrhard, Christine Tasson, Michele Pagani |
| 2014 | Probabilistic relational verification for cryptographic implementations. Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin |
| 2014 | Profiling for laziness. Stephen Chang, Matthias Felleisen |
| 2014 | Proof search for propositional abstract separation logics via labelled sequents. Zhe Hou, Ranald Clouston, Rajeev Goré, Alwen Tiu |
| 2014 | Proofs that count. Azadeh Farzan, Zachary Kincaid, Andreas Podelski |
| 2014 | Replicated data types: specification, verification, optimality. Sebastian Burckhardt, Alexey Gotsman, Hongseok Yang, Marek Zawirski |
| 2014 | Sound compilation of reals. Eva Darulova, Viktor Kuncak |
| 2014 | Sound input filter generation for integer overflow errors. Fan Long, Stelios Sidiroglou-Douskos, Deokhwan Kim, Martin C. Rinard |
| 2014 | Symbolic optimization with SMT solvers. Yi Li, Aws Albarghouthi, Zachary Kincaid, Arie Gurfinkel, Marsha Chechik |
| 2014 | Tabular: a schema-driven probabilistic programming language. Andrew D. Gordon, Thore Graepel, Nicolas Rolland, Claudio V. Russo, Johannes Borgström, John Guiver |
| 2014 | The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014 Suresh Jagannathan, Peter Sewell |
| 2014 | The essence of Reynolds. Stephen Brookes, Peter W. O'Hearn, Uday S. Reddy |
| 2014 | Toward general diagnosis of static errors. Danfeng Zhang, Andrew C. Myers |
| 2014 | Tracing compilation by abstract interpretation. Stefano Dissegna, Francesco Logozzo, Francesco Ranzato |
| 2014 | Verifying eventual consistency of optimistic replication systems. Ahmed Bouajjani, Constantin Enea, Jad Hamza |