Abstract is missing.
- (Co-)Iteration for Higher-Order Nested DatatypesAndreas Abel, Ralph Matthes. 1-20 [doi]
- Program Extraction in Simply-Typed Higher Order LogicStefan Berghofer. 21-38 [doi]
- General Recursion in Type TheoryAna Bove. 39-58 [doi]
- Using Theory Morphisms for Implementing Formal Methods ToolsAchim D. Brucker, Burkhart Wolff. 59-77 [doi]
- Subsets, Quotients and Partial Functions in Martin-Löf s Type TheoryJesper Carlström. 78-94 [doi]
- Mathematical Quotients and Quotient Types in CoqLaurent Chicli, Loic Pottier, Carlos Simpson. 95-107 [doi]
- A Constructive Formalization of the Fundamental Theorem of CalculusLuís Cruz-Filipe. 108-126 [doi]
- Two Behavioural Lambda ModelsMariangiola Dezani-Ciancaglini, Silvia Ghilezan. 127-147 [doi]
- A Unifying Approach to Recursive and Co-recursive DefinitionsPietro Di Gianantonio, Marino Miculan. 148-161 [doi]
- Holes with Binding PowerGueorgui I. Jojgov. 162-181 [doi]
- Typing with Conditions and Guarantees for Functional In-place UpdateMichal Konecný. 182-199 [doi]
- A New Extraction for CoqPierre Letouzey. 200-219 [doi]
- Weak Transitivity in Coercive SubtypingYong Luo, Zhaohui Luo, Sergei Soloviev. 220-239 [doi]
- The Not So Simple Proof-Irrelevant Model of CCAlexandre Miquel, Benjamin Werner. 240-258 [doi]
- Structured Proofs in Isar/HOLTobias Nipkow. 259-278 [doi]
- Java as a Functional Programming LanguageAnton Setzer. 279-298 [doi]
- Monad Translating Inductive and Coinductive TypesTarmo Uustalu. 299-315 [doi]
- A Finite First-Order Presentation of Set TheoryStéphane Vaillant. 316-330 [doi]