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

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

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

Last update Sat May 25 21:13:27 2013 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page