Volume 58, Number 1, 2001

MERLIN 2001: Mechanized Reasoning about Languages with Variable Binding, Siena, 18/6/2001, held in connection with IJCAR 2001

• 
  Christine Röckl: A First-Order Syntax for the Pi-Calculus in Isabelle/HOL using Permutations. 1-17
• 
  René Vestergaard, James Brotherston: The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective). 18-36
• 
  Marino Miculan: Developing (Meta)Theory of Lambda-calculus in the Theory of Context. 37-58
• 
  Dale Miller: Encoding Generic Judgments: Preliminary results. ... 59-78
• 
  Carsten Schürmann, Dachuan Yu, Zhaozhong Ni: A Representation of Fomega in LF. 79-96
• 
  Andreas Abel: A Third-Order Representation of the lambda-mu-Calculus. 97-114
• 
  Simon Ambler, Roy L. Crole, Alberto Momigliano: Preface: Mechanised Reasoning about Languages with Variable Binding 2001. 115-116

Volume 58, Number 2, 2001

4th International Workshop on Strategies in Automated Deduction (STRATEGIES 2001) - Selected Papers, Siena, Italy, June 18, 2001

• 
  Wolfgang Goerigk: Mechanical Software Verification: High Level Control Aspects from a User's Perspective. 117-137
• 
  Richard B. Kieburtz: A Logic for Rewriting Strategies. 138-154
• 
  Olivier Fissore, Isabelle Gnaedig, Hélène Kirchner: Termination of Rewriting with Local Strategies. 155-188
• 
  Serge Autexier: A Proof-Planning Framework with Explicit Abstractions Based on Indexed Formulas. 189-202
• 
  Axel Schairer, Serge Autexier, Dieter Hutter: A Pragmatic Approach to Reuse in Tactical Theorem Proving. 203-216
• 
  Maria Paola Bonacina, Bernhard Gramlich: Preface: STRATEGIES 2001. 217-218