Abstract is missing.
- Type-Directed Compilation in the Wild: Haskell and CoreSimon L. Peyton Jones. 1 [doi]
- Proving with Side EffectsHugo Herbelin. 2 [doi]
- Non-linearity as the Metric Completion of LinearityDamiano Mazza. 3-14 [doi]
- i Ki Yung Ahn, Tim Sheard, Marcelo P. Fiore, Andrew M. Pitts. 15-30 [doi]
- Non-determinism, Non-termination and the Strong Normalization of System TFederico Aschieri, Margherita Zorzi. 31-47 [doi]
- Proof-Relevant Logical Relations for Name GenerationNick Benton, Martin Hofmann, Vivek Nigam. 48-60 [doi]
- Games with Sequential Backtracking and Complete Game Semantics for Subclassical LogicsStefano Berardi, Makoto Tatsuta. 61-76 [doi]
- Realizability for Peano Arithmetic with Winning Conditions in HON GamesValentin Blot. 77-92 [doi]
- The Resource Lambda Calculus Is Short-Sighted in Its Relational ModelFlavien Breuvart. 93-108 [doi]
- Bounding Skeletons, Locally Scoped Terms and Exact Bounds for Linear Head ReductionPierre Clairambault. 109-124 [doi]
- Intersection Type Matching with SubtypingBoris Düdder, Moritz Martens, Jakob Rehof. 125-139 [doi]
- A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by EvaluationDaniel Fridlender, Miguel Pagano. 140-155 [doi]
- Small Induction RecursionPeter Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta, Thorsten Altenkirch. 156-172 [doi]
- Generalizations of Hedberg's TheoremNicolai Kraus, Martín Hötzel Escardó, Thierry Coquand, Thorsten Altenkirch. 173-188 [doi]
- Using Models to Model-Check Recursive SchemesSylvain Salvati, Igor Walukiewicz. 189-204 [doi]
- On Interaction, Continuations and DefunctionalizationUlrich Schöpp. 205-220 [doi]
- Completeness of Conversion between Reactive Programs for Ultrametric ModelsPaula Severi, Fer-Jan de Vries. 221-235 [doi]
- A Constructive Model of Uniform ContinuityChuangjie Xu, Martín Hötzel Escardó. 236-249 [doi]