Abstract is missing.
- Experiments in Information Flow AnalysisAnnabelle McIver. 1-17 [doi]
- Handling Local State with Global StateKoen Pauwels, Tom Schrijvers, Shin-Cheng Mu. 18-44 [doi]
- Certification of Breadth-First Algorithms by ExtractionDominique Larchey-Wendling, Ralph Matthes. 45-75 [doi]
- Verified Self-Explaining ComputationJan Stolarek, James Cheney. 76-102 [doi]
- Self-certifying Railroad Diagrams - Or: How to Teach Nondeterministic Finite AutomataRalf Hinze. 103-137 [doi]
- How to Calculate with Nondeterministic FunctionsRichard Bird, Florian Rabe. 138-154 [doi]
- Setoid Type Theory - A Syntactic TranslationThorsten Altenkirch, Simon Boulier, Ambrus Kaposi, Nicolas Tabareau. 155-196 [doi]
- Cylindric Kleene Lattices for Program ConstructionBrijesh Dongol, Ian J. Hayes, Larissa Meinicke, Georg Struth. 197-225 [doi]
- A Hierarchy of Monadic Effects for Program Verification Using Equational ReasoningReynald Affeldt, David Nowak, Takafumi Saikawa. 226-254 [doi]
- System F in Agda, for Fun and ProfitJames Chapman, Roman Kireev, Chad Nester, Philip Wadler. 255-297 [doi]
- An Analysis of Repeated Graph SearchRoland Carl Backhouse. 298-328 [doi]
- Shallow Embedding of Type Theory is Morally CorrectAmbrus Kaposi, András Kovács, Nicolai Kraus. 329-365 [doi]
- En Garde! Unguarded Iteration for Reversible Computation in the Delay MonadRobin Kaarsgaard, Niccolò Veltri. 366-384 [doi]
- Completeness and Incompleteness of Synchronous Kleene AlgebraJana Wagemaker, Marcello M. Bonsangue, Tobias Kappé, Jurriaan Rot, Alexandra Silva 0001. 385-413 [doi]
- Unraveling Recursion: Compiling an IR with Recursion to System FMichael Peyton Jones, Vasilis Gkoumas, Roman Kireev, Kenneth Mackenzie, Chad Nester, Philip Wadler. 414-443 [doi]
- Coding with Asymmetric Numeral SystemsJeremy Gibbons. 444-465 [doi]