Abstract is missing.
- Algorithmic Equality in Heyting Arithmetic ModuloLisa Allali. 1-17 [doi]
- CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent TypesRobert Atkey. 18-32 [doi]
- Dependently Sorted LogicJoão Filipe Belo. 33-50 [doi]
- Finiteness in a Minimalist FoundationFrancesco Ciraulo, Giovanni Sambin. 51-68 [doi]
- A Declarative Language for the Coq Proof AssistantPierre Corbineau. 69-84 [doi]
- Characterising Strongly Normalising Intuitionistic Sequent TermsJosé Espírito Santo, Silvia Ghilezan, J. Ivetic. 85-99 [doi]
- Intuitionistic vs. Classical Tautologies, Quantitative ComparisonAntoine Genitrini, Jakub Kozik, Marek Zaionc. 100-109 [doi]
- In the Search of a Naive Type TheoryAgnieszka Kozubek, Pawel Urzyczyn. 110-124 [doi]
- Verification of the Redecoration Algorithm for Triangular MatricesRalph Matthes, Martin Strecker. 125-141 [doi]
- A Logic for Parametric Polymorphism with EffectsRasmus Ejlers Møgelberg, Alex Simpson. 142-156 [doi]
- Working with Mathematical Structures in Type TheoryClaudio Sacerdoti Coen, Enrico Tassi. 157-172 [doi]
- On Normalization by Evaluation for Object CalculiJan Schwinghammer. 173-187 [doi]
- Attributive Types for Proof ErasureHongwei Xi. 188-202 [doi]