| 2017 | Faster Algorithms for Weighted Recursive State Machines. | Krishnendu Chatterjee, Bernhard Kragl, Samarth Mishra, Andreas Pavlogiannis |
| 2017 | Temporary Read-Only Permissions for Separation Logic. | Arthur Charguraud, Franois Pottier |
| 2017 | Linearity, Control Effects, and Behavioral Types. | Lus Caires, Jorge A. Prez |
| 2017 | Incremental Update for Graph Rewriting. | Pierre Boutillier, Thomas Ehrhard, Jean Krivine |
| 2017 | Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency. | Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, Serdar Tasiran |
| 2017 | Confluence of Graph Rewriting with Interfaces. | Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, Fabio Zanasi |
| 2017 | Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants. | Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, Dmitriy Traytel |
| 2017 | Observed Communication Semantics for Classical Processes. | Robert Atkey |
| 2017 | Generalizing Inference Systems by Coaxioms. | Davide Ancona, Francesco Dagnino, Elena Zucca |
| 2017 | Disjoint Polymorphism. | Joo Alpuim, Bruno C. d. S. Oliveira, Zhiyuan Shi |
| 2017 | Programs Using Syntax with First-Class Binders. | Francisco Ferreira, Brigitte Pientka |
| 2016 | A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs. | Yuting Wang, Gopalan Nadathur |
| 2016 | Transfinite Step-Indexing: Decoupling Concrete and Logical Steps. | Kasper Svendsen, Filip Sieczkowski, Lars Birkedal |
| 2016 | Actor Services - Modular Verification of Message Passing Programs. | Alexander J. Summers, Peter Mller |
| 2016 | Type Error Diagnosis for Embedded DSLs by Two-Stage Specialized Type Rules. | Alejandro Serrano, Jurriaan Hage |
| 2016 | Macrofication: Refactoring by Reverse Macro Expansion. | Christopher Schuster, Tim Disney, Cormac Flanagan |
| 2016 | The Expressive Power of Monotonic Parallel Composition. | Johannes man Pohjola, Joachim Parrow |
| 2016 | Modular Termination Verification for Non-blocking Concurrency. | Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, Julian Sutherland |
| 2016 | Classical By-Need. | Pierre-Marie Pdrot, Alexis Saurin |
| 2016 | Functional Big-Step Semantics. | Scott Owens, Magnus O. Myreen, Ramana Kumar, Yong Kiam Tan |
| 2016 | An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs. | Antoine Min, Jason Breck, Thomas W. Reps |
| 2016 | Extensible and Efficient Automation Through Reflective Tactics. | Gregory Malecha, Jesper Bengtson |
| 2016 | Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach. | Cludio Belo Loureno, Maria Joo Frade, Jorge Sousa Pinto |
| 2016 | Simulating Cities: A Software Engineering Perspective. | Cristina V. Lopes |
| 2016 | Probabilistic Functions and Cryptographic Oracles in Higher Order Logic. | Andreas Lochbihler |