Abstract is missing.
- A Modular Hierarchy of Logical FrameworksRobin Adams. 1-16 [doi]
- Tailoring Filter ModelsFabio Alessi, Franco Barbanera, Mariangiola Dezani-Ciancaglini. 17-33 [doi]
- Locales and Locale Expressions in Isabelle/IsarClemens Ballarin. 34-50 [doi]
- Introduction to PAF!, a Proof Assistant for ML Programs VerificationSylvain Baro. 51-65 [doi]
- A Constructive Proof of Higman s Lemma in IsabelleStefan Berghofer. 66-82 [doi]
- A Core Calculus of Higher-Order Mixins and ClassesLorenzo Bettini, Viviana Bono, Silvia Likavec. 83-98 [doi]
- Type Inference for Nested Self TypesViviana Bono, Jerzy Tiuryn, Pawel Urzyczyn. 99-114 [doi]
- Inductive Families Need Not Store Their IndicesEdwin Brady, Conor McBride, James McKinna. 115-129 [doi]
- Modules in Coq Are and Will Be CorrectJacek Chrzaszcz. 130-146 [doi]
- Rewriting Calculus with Fixpoints: Untyped and First-Order SystemsHoratiu Cirstea, Luigi Liquori, Benjamin Wack. 147-161 [doi]
- First-Order Reasoning in the Calculus of Inductive ConstructionsPierre Corbineau. 162-177 [doi]
- Higher-Order Linear Ramified RecurrenceUgo Dal Lago, Simone Martini, Luca Roversi. 178-193 [doi]
- Confluence and Strong Normalisation of the Generalised Multiary ?-CalculusJosé Espírito Santo, Luis Pinto. 194-209 [doi]
- Wellfounded Trees and Dependent Polynomial FunctorsNicola Gambino, Martin Hyland. 210-225 [doi]
- Classical Proofs, Typed Processes, and Intersection Types: Extended AbstractSilvia Ghilezan, Pierre Lescanne. 226-241 [doi]
- Wave-Style Geometry of Interaction Models in Rel Are Graph-Like Lambda-ModelsFurio Honsell, Marina Lenisa. 242-258 [doi]
- Coercions in Hindley-Milner SystemsRobert Kießling, Zhaohui Luo. 259-275 [doi]
- Combining Incoherent Coercions for Sigma-TypesYong Luo, Zhaohui Luo. 276-292 [doi]
- Induction and Co-induction in Sequent CalculusAlberto Momigliano, Alwen Fernanto Tiu. 293-308 [doi]
- QArith: Coq Formalisation of Lazy Rational ArithmeticMilad Niqui, Yves Bertot. 309-323 [doi]
- Mobility Types in CoqFurio Honsell, Ivan Scagnetto. 324-337 [doi]
- Some Algebraic Structures in Lambda-Calculus with Inductive TypesSergei Soloviev, David Chemouil. 338-354 [doi]
- A Concurrent Logical Framework: The Propositional FragmentKevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker. 355-377 [doi]
- Formal Proof SketchesFreek Wiedijk. 378-393 [doi]
- Applied Type System: Extended AbstractHongwei Xi. 394-408 [doi]