| 2018 | Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine. | Fabian Kunze, Gert Smolka, Yannick Forster |
| 2018 | Traf: A Graphical Proof Tree Viewer Cooperating with Coq Through Proof General. | Hideyuki Kawabata, Yuta Tanaka, Mai Kimura, Tetsuo Hironaka |
| 2018 | New Approaches for Almost-Sure Termination of Probabilistic Programs. | Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee |
| 2018 | Shallow Effect Handlers. | Daniel Hillerstrm, Sam Lindley |
| 2018 | Automated Synthesis of Functional Programs with Auxiliary Functions. | Shingo Eguchi, Naoki Kobayashi, Takeshi Tsukada |
| 2018 | Non-linear Pattern Matching with Backtracking for Non-free Data Types. | Satoshi Egi, Yuichi Nishiwaki |
| 2018 | Automated Modular Verification for Relaxed Communication Protocols. | Andreea Costea, Wei-Ngan Chin, Shengchao Qin, Florin Craciun |
| 2018 | HoIce: An ICE-Based Non-linear Horn Clause Solver. | Adrien Champion, Naoki Kobayashi, Ryosuke Sato |
| 2018 | On the Complexity of Pointer Arithmetic in Separation Logic. | James Brotherston, Max I. Kanovich |
| 2018 | Factoring Derivation Spaces via Intersection Types. | Pablo Barenbaum, Gonzalo Ciruelos |
| 2018 | Scallina: Translating Verified Programs from Coq to Scala. | Youssef El Bakouny, Dani Mezher |
| 2018 | Types of Fireballs. | Beniamino Accattoli, Giulio Guerrieri |
| 2018 | The Practice of a Compositional Functional Programming Language. | Timothy Jones, Michael Homer |
| 2017 | Palgol: A High-Level DSL for Vertex-Centric Graph Processing with Remote Data Access. | Yongzhe Zhang, Hsiang-Shang Ko, Zhenjiang Hu |
| 2017 | Synthesizing SystemC Code from Delay Hybrid CSP. | Gaogao Yan, Li Jiao, Shuling Wang, Naijun Zhan |
| 2017 | Partiality and Container Monads. | Tarmo Uustalu, Niccol Veltri |
| 2017 | A Computational Interpretation of Context-Free Expressions. | Martin Sulzmann, Peter Thiemann |
| 2017 | Efficient Functional Reactive Programming Through Incremental Behaviors. | Bob Reynders, Dominique Devriese |
| 2017 | Static Analysis of Multithreaded Recursive Programs Communicating via Rendez-Vous. | Adrien Pommellet, Tayssir Touili |
| 2017 | Sharper and Simpler Nonlinear Interpolants for Program Verification. | Takamasa Okudono, Yuki Nishida, Kensuke Kojima, Kohei Suenaga, Kengo Kido, Ichiro Hasuo |
| 2017 | Verified Root-Balanced Trees. | Tobias Nipkow |
| 2017 | A Nonstandard Functional Programming Language. | Hirofumi Nakamura, Kensuke Kojima, Kohei Suenaga, Atsushi Igarashi |
| 2017 | Programming and Proving with Classical Types. | Cristina Matache, Victor B. F. Gomes, Dominic P. Mulligan |
| 2017 | Taming Message-Passing Communication in Compositional Reasoning About Confidentiality. | Ximeng Li, Heiko Mantel, Markus Tasch |
| 2017 | Implementing Algebraic Effects in C - "Monads for Free in C". | Daan Leijen |