| 2014 | Modular, higher-order cardinality analysis in theory and practice. | Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones |
| 2014 | Formal Analysis of CRT-RSA Vigilant's Countermeasure Against the BellCoRe Attack: A Pledge for Formal Methods in the Field of Implementation Security. | Pablo Rauzy, Sylvain Guilley |
| 2014 | A type-directed abstraction refinement approach to higher-order model checking. | Steven J. Ramsay, Robin P. Neatherway, C.-H. Luke Ong |
| 2014 | Analyzing program dependencies for malware detection. | Mila Dalla Preda, Isabella Mastroeni, Roberto Giacobazzi |
| 2014 | Applying quantitative semantics to higher-order quantum computing. | Michele Pagani, Peter Selinger, Benot Valiron |
| 2014 | Game semantics for interface middleweight Java. | Andrzej S. Murawski, Nikos Tzevelekos |
| 2014 | Authenticated data structures, generically. | Andrew Miller, Michael Hicks, Jonathan Katz, Elaine Shi |
| 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 | A proof system for separation logic with magic wand. | Wonyeol Lee, Sungwoo Park |
| 2014 | On coinductive equivalences for higher-order probabilistic functional programs. | Ugo Dal Lago, Davide Sangiorgi, Michele Alberti |
| 2014 | Freeze after writing: quasi-deterministic parallel programming with LVars. | Lindsey Kuper, Aaron Turon, Neelakantan R. Krishnaswami, Ryan R. Newton |
| 2014 | CakeML: a verified implementation of ML. | Ramana Kumar, Magnus O. Myreen, Michael Norrish, Scott Owens |
| 2014 | An operational and axiomatic semantics for non-determinism and sequence points in C. | Robbert Krebbers |
| 2014 | Backpack: retrofitting Haskell with interfaces. | Scott Kilpatrick, Derek Dreyer, Simon L. Peyton Jones, Simon Marlow |
| 2014 | Parametric effect monads and semantics of effect systems. | Shin-ya Katsumata |
| 2014 | Recovering C++ Objects From Binaries Using Inter-Procedural Data-Flow Analysis. | Wesley Jin, Cory F. Cohen, Jeffrey Gennari, Charles Hines, Sagar Chaki, Arie Gurfinkel, Jeffrey Havrilla, Priya Narasimhan |
| 2014 | Abstract acceleration of general linear loops. | Bertrand Jeannet, Peter Schrammel, Sriram Sankaranarayanan |
| 2014 | Modular reasoning about heap paths via effectively propositional formulas. | Shachar Itzhaky, Anindya Banerjee, Neil Immerman, Ori Lahav, Aleksandar Nanevski, Mooly Sagiv |
| 2014 | 30 years of research and development around Coq. | Grard P. Huet, Hugo Herbelin |
| 2014 | Proof search for propositional abstract separation logics via labelled sequents. | Zhe Hou, Ranald Clouston, Rajeev Gor, Alwen Tiu |
| 2014 | Tabular: a schema-driven probabilistic programming language. | Andrew D. Gordon, Thore Graepel, Nicolas Rolland, Claudio V. Russo, Johannes Borgstrm, John Guiver |
| 2014 | Proofs that count. | Azadeh Farzan, Zachary Kincaid, Andreas Podelski |
| 2014 | Closed type families with overlapping equations. | Richard A. Eisenberg, Dimitrios Vytiniotis, Simon L. Peyton Jones, Stephanie Weirich |
| 2014 | Probabilistic coherence spaces are fully abstract for probabilistic PCF. | Thomas Ehrhard, Christine Tasson, Michele Pagani |