Proceedings

• Cover Page and Program
  
• The Context Calculus Lambda-c
  Mirna Bognar and Roel de Vrijer (Vrije University, The Netherlands)
• Explicit Substitutions for Linear Logical Frameworks
  Iliano Cervesato (Stanford University, USA), Valeria de Paiva (University of Birmingham, UK), and Eike Ritter (University of Birmingham, UK)
• JaLoF: A Development Environment for Deduction Systems
  Roderick Moten (Colgate University, USA)
• Structured Type Theory
  Catarina Coquand and Thierry Coquand (Chalmers University and University of Goteborg, Sweden)
• Reflective Metalogical Frameworks
  David Basin (University of Freiburg, Germany), Manuel Clavel (University of Navarre, Spain), and José Meseguer (SRI International, USA)
• A Logic Programming Approach to Implementing Higher-Order Narrowing
  Murat Sinan Aygun (Bogazici University, Turkey)
• The Type Theory and Type Checker of GF
  Petri Mäenpää (Nokia Telecommunications, Finland) and Aarne Ranta (Chalmers University and University of Goteborg, Sweden)
• Pure Type Systems in Rewriting Logic
  Mark-Oliver Stehr and José Meseguer (SRI International, USA)
• On Equivalence and Canonical Forms in the LF Type Theory
  Robert Harper and Frank Pfenning (Carnegie Mellon University, USA)
• Type Checking Meta Programs
  Nikolaj Bjorner (Kestrel Institute, USA)

Special Issue

A special issue of the Journal of Automated Reasoning (Volume 27, Issue 1, July 2001) on the topic of the workshop was published following the workshop.