| 2010 | The Logic of Large Enough. | Eerke A. Boiten, Dan Grundy |
| 2010 | On Automated Program Construction and Verification. | Rudolf Berghammer, Georg Struth |
| 2010 | The Algorithmics of Solitaire-Like Games. | Roland Carl Backhouse, Wei Chen, Joo F. Ferreira |
| 2008 | Symmetric and Synchronous Communication in Peer-to-Peer Networks. | Andreas Witzel |
| 2008 | Asymptotic Improvement of Computations over Free Monads. | Janis Voigtlnder |
| 2008 | Synthesis of Optimal Control Policies for Some Infinite-State Transition Systems. | Michel Sintzoff |
| 2008 | A Hoare Logic for Call-by-Value Functional Programs. | Yann Rgis-Gianas, Franois Pottier |
| 2008 | Safe Modification of Pointer Programs in Refinement Calculus. | Susumu Nishimura |
| 2008 | Algebra of Programming Using Dependent Types. | Shin-Cheng Mu, Hsiang-Shang Ko, Patrik Jansson |
| 2008 | Programming with Effects in Coq. | Greg Morrisett |
| 2008 | Probabilistic Choice in Refinement Algebra. | Larissa Meinicke, Ian J. Hayes |
| 2008 | Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening. | Ralph Matthes |
| 2008 | The Expression Lemma. | Ralf Lmmel, Ondrej Rypacek |
| 2008 | The Bhm-Jacopini Theorem Is False, Propositionally. | Dexter Kozen, Wei-Lung Dustin Tseng |
| 2008 | Scrap Your Type Applications. | Barry Jay, Simon L. Peyton Jones |
| 2008 | Exploiting Unique Fixed Points. | Ralf Hinze |
| 2008 | Asynchronous Exceptions as an Effect. | William L. Harrison, Gerard Allwein, Andy Gill, Adam M. Procter |
| 2008 | Circulations, Fuzzy Relations and Semirings. | Roland Glck, Bernhard Mller |
| 2008 | Unfolding Abstract Datatypes. | Jeremy Gibbons |
| 2008 | Modal Semirings Revisited. | Jules Desharnais, Georg Struth |
| 2008 | Zippy Tabulations of Recursive Functions. | Richard S. Bird |
| 2008 | Recounting the Rationals: Twice!. | Roland Carl Backhouse, Joo F. Ferreira |
| 2008 | The Capacity-CTorch Problem. | Roland Carl Backhouse |
| 2008 | Verifying a Semantic beta-eta-Conversion Test for Martin-Lf Type Theory. | Andreas Abel, Thierry Coquand, Peter Dybjer |
| 2006 | Quantum Predicative Programming. | Anya Tafliovich, Eric C. R. Hehner |