| 2013 | A nanopass framework for commercial compiler development. Andrew W. Keep, R. Kent Dybvig |
| 2013 | A practical theory of language-integrated query. James Cheney, Sam Lindley, Philip Wadler |
| 2013 | A short cut to parallelization theorems. Akimasa Morihata |
| 2013 | ACM SIGPLAN International Conference on Functional Programming, ICFP'13, Boston, MA, USA - September 25 - 27, 2013 Greg Morrisett, Tarmo Uustalu |
| 2013 | Automatic SIMD vectorization for Haskell. Leaf Petersen, Dominic A. Orchard, Neal Glew |
| 2013 | C-SHORe: a collapsible approach to higher-order verification. Christopher H. Broadbent, Arnaud Carayol, Matthew Hague, Olivier Serre |
| 2013 | Calculating threesomes, with blame. Ronald Garcia |
| 2013 | Complete and easy bidirectional typechecking for higher-rank polymorphism. Jana Dunfield, Neelakantan R. Krishnaswami |
| 2013 | Computer science as a school subject. Simon L. Peyton Jones |
| 2013 | Correctness of an STM Haskell implementation. Manfred Schmidt-Schauß, David Sabel |
| 2013 | Efficient divide-and-conquer parsing of practical context-free languages. Jean-Philippe Bernardy, Koen Claessen |
| 2013 | Experience report: applying random testing to a base type environment. Vincent St-Amour, Neil Toronto |
| 2013 | Experience report: functional programming of mHealth applications. Chris Petersen, Matthias Görges, Dustin T. Dunsmuir, John Mark Ansermino, Guy Albert Dumont |
| 2013 | Exploiting vector instructions with generalized stream fusio. Geoffrey Mainland, Roman Leshchinskiy, Simon L. Peyton Jones |
| 2013 | Fun with semirings: a functional pearl on the abuse of linear algebra. Stephen Dolan |
| 2013 | Functional geometry and the Traité de Lutherie: functional pearl. Harry G. Mairson |
| 2013 | Functional reactive programming with liveness guarantees. Alan Jeffrey |
| 2013 | Handlers in action. Ohad Kammar, Sam Lindley, Nicolas Oury |
| 2013 | Higher-order functional reactive programming without spacetime leaks. Neelakantan R. Krishnaswami |
| 2013 | Hoare-style reasoning with (algebraic) continuations. Germán Andrés Delbianco, Aleksandar Nanevski |
| 2013 | Interactive programming with dependent types. Ulf Norell |
| 2013 | Modular and automated type-soundness verification for language extensions. Florian Lorenzen, Sebastian Erdweg |
| 2013 | Modular monadic meta-theory. Benjamin Delaware, Steven Keuchel, Tom Schrijvers, Bruno C. d. S. Oliveira |
| 2013 | Mtac: a monad for typed tactic programming in Coq. Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis |
| 2013 | Optimising purely functional GPU programs. Trevor L. McDonell, Manuel M. T. Chakravarty, Gabriele Keller, Ben Lippmeier |
| 2013 | Optimizing abstract abstract machines. Dionna Amalie Glaze, Nicholas Labich, Matthew Might, David Van Horn |
| 2013 | Productive coprogramming with guarded recursion. Robert Atkey, Conor McBride |
| 2013 | Programming and reasoning with algebraic effects and dependent types. Edwin C. Brady |
| 2013 | Programming with permissions in Mezzo. François Pottier, Jonathan Protzenko |
| 2013 | Simple and compositional reification of monadic embedded languages. Josef Svenningsson, Bo Joel Svensson |
| 2013 | Structural recursion for querying ordered graphs. Soichiro Hidaka, Kazuyuki Asada, Zhenjiang Hu, Hiroyuki Kato, Keisuke Nakano |
| 2013 | System FC with explicit kind equality. Stephanie Weirich, Justin Hsu, Richard A. Eisenberg |
| 2013 | Testing noninterference, quickly. Catalin Hritcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, Leonidas Lampropoulos |
| 2013 | The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier. Adam Chlipala |
| 2013 | The constrained-monad problem. Neil Sculthorpe, Jan Bracker, George Giorgidze, Andy Gill |
| 2013 | Type-theory in color. Jean-Philippe Bernardy, Guilhem Moulin |
| 2013 | Typed syntactic meta-programming. Dominique Devriese, Frank Piessens |
| 2013 | Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. Aaron Turon, Derek Dreyer, Lars Birkedal |
| 2013 | Unifying structured recursion schemes. Ralf Hinze, Nicolas Wu, Jeremy Gibbons |
| 2013 | Using circular programs for higher-order syntax: functional pearl. Emil Axelsson, Koen Claessen |
| 2013 | Verified decision procedures for MSO on words based on derivatives of regular expressions. Dmitriy Traytel, Tobias Nipkow |
| 2013 | Weak optimality, and the meaning of sharing. Thibaut Balabonski |
| 2013 | Wellfounded recursion with copatterns: a unified approach to termination and productivity. Andreas Abel, Brigitte Pientka |