Abstract is missing.
- Weyl s Predicative Classical Mathematics as a Logic-Enriched Type TheoryRobin Adams, Zhaohui Luo. 1-17 [doi]
- Crafting a Proof AssistantAndrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli. 18-32 [doi]
- On Constructive Cut Admissibility in Deduction ModuloRichard Bonichon, Olivier Hermant. 33-47 [doi]
- Fast Reflexive Arithmetic Tactics the Linear Case and BeyondFrédéric Besson. 48-62 [doi]
- Combining de Bruijn Indices and Higher-Order Abstract Syntax in CoqVenanzio Capretta, Amy P. Felty. 63-77 [doi]
- Deciding Equality in the Constructor TheoryPierre Corbineau. 78-92 [doi]
- A Formalisation of a Dependently Typed Language as an Inductive-Recursive FamilyNils Anders Danielsson. 93-109 [doi]
- Truth Values Algebras and Proof NormalizationGilles Dowek. 110-124 [doi]
- Curry-Style Types for Nominal TermsMaribel Fernández, Murdoch Gabbay. 125-139 [doi]
- (In)consistency of Extensions of Higher Order Logic and Type TheoryHerman Geuvers. 140-159 [doi]
- Constructive Type Classes in IsabelleFlorian Haftmann, Makarius Wenzel. 160-174 [doi]
- Zermelo s Well-Ordering Theorem in Type TheoryDanko Ilik. 175-187 [doi]
- A Finite First-Order Theory of ClassesFlorent Kirchner. 188-202 [doi]
- Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real NumbersMilad Niqui. 203-220 [doi]
- Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional ProgramsHugo R. Simões, Kevin Hammond, Mário Florido, Pedro B. Vasconcelos. 221-236 [doi]
- Subset Coercions in CoqMatthieu Sozeau. 237-252 [doi]
- A Certified Distributed Security Logic for Authorizing CodeNathan Whitehead. 253-268 [doi]