| 2013 | Mtac: a monad for typed tactic programming in Coq. | Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis |
| 2013 | System FC with explicit kind equality. | Stephanie Weirich, Justin Hsu, Richard A. Eisenberg |
| 2013 | Towards systematic parallel programming of graph problems via tree decomposition and tree parallelism. | Qi Wang, Meixian Chen, Yu Liu, Zhenjiang Hu |
| 2013 | Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. | Aaron Turon, Derek Dreyer, Lars Birkedal |
| 2013 | Verified decision procedures for MSO on words based on derivatives of regular expressions. | Dmitriy Traytel, Tobias Nipkow |
| 2013 | Counting and occurrence sort for GPUs using an embedded language. | Josef David Svenningsson, Bo Joel Svensson, Mary Sheeran |
| 2013 | Simple and compositional reification of monadic embedded languages. | Josef Svenningsson, Bo Joel Svensson |
| 2013 | Experience report: applying random testing to a base type environment. | Vincent St-Amour, Neil Toronto |
| 2013 | Semantics-preserving data layout transformations for improved vectorisation. | Artjoms Sinkarovs, Sven-Bodo Scholz |
| 2013 | The constrained-monad problem. | Neil Sculthorpe, Jan Bracker, George Giorgidze, Andy Gill |
| 2013 | Correctness of an STM Haskell implementation. | Manfred Schmidt-Schau, David Sabel |
| 2013 | Grammar-based automated music composition in Haskell. | Donya Quick, Paul Hudak |
| 2013 | Programming with permissions in Mezzo. | Franois Pottier, Jonathan Protzenko |
| 2013 | Automatic SIMD vectorization for Haskell. | Leaf Petersen, Dominic A. Orchard, Neal Glew |
| 2013 | Experience report: functional programming of mHealth applications. | Chris Petersen, Matthias Grges, Dustin T. Dunsmuir, John Mark Ansermino, Guy Albert Dumont |
| 2013 | Interactive programming with dependent types. | Ulf Norell |
| 2013 | A short cut to parallelization theorems. | Akimasa Morihata |
| 2013 | Optimising purely functional GPU programs. | Trevor L. McDonell, Manuel M. T. Chakravarty, Gabriele Keller, Ben Lippmeier |
| 2013 | Functional geometry and the Trait de Lutherie: functional pearl. | Harry G. Mairson |
| 2013 | Exploiting vector instructions with generalized stream fusio. | Geoffrey Mainland, Roman Leshchinskiy, Simon L. Peyton Jones |
| 2013 | Towards a streaming model for nested data parallelism. | Frederik M. Madsen, Andrzej Filinski |
| 2013 | Modular and automated type-soundness verification for language extensions. | Florian Lorenzen, Sebastian Erdweg |
| 2013 | QuaFL: a typed DSL for quantum programming. | Andrei Lapets, Marcus P. da Silva, Mike Thome, Aaron Adler, Jacob Beal, Martin Roetteler |
| 2013 | Abstract resource cost derivation for logical quantum circuit descriptions. | Andrei Lapets, Martin Roetteler |
| 2013 | LVars: lattice-based data structures for deterministic parallelism. | Lindsey Kuper, Ryan R. Newton |