Electronic Notes in Theoretical Computer Science, Volume 58

Volume 58, Number 1, 2001

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

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

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

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