Regular papers

David Delahaye, Chalmers U of Techn., Sweden
A proof dedicated meta-language

Pablo López, U Málaga, Spain; Ernesto Pimentel, U Málaga, Spain; Joshua S. Hodas, Harvey Mudd College, USA; Jeffrey Polakow, GNP Computers, USA; and Lubomira Stoilova, Harvey Mudd College, USA
Isolating resource comsumption in linear-logic proof search

Alberto Momigliano, Simon J. Ambler, and Roy L. Crole; U Leicester, UK
A hybrid encoding of Howe's method for establishing congruence of bisimilarity

Brigitte Pientka, Carnegie Mellon U, USA
Memoization-based proof search in LF: An experimental evaluation of a prototype

Ivan Scagnetto and Marino Miculan, U Udine, Italy
Ambient Calculus and its logic in the Calculus of Inductive Constructions

Carsten Schürmann, Yale U, USA and Serge Autexier, DFKI Saarbrücken, Germany
Towards proof planning for M_ω⁺

Aaron Stump and David L. Dill, Stanford U, USA
Producing proofs from an arithmetic decision procedure in elliptical LF

Femke van Raamsdonk, Vrije U of Amsterdam, The Netherlands and Paula Severi, U Turin, Italy
Eliminating proofs from programs

Joseph C. Vanderwaart and Karl Crary, Carnegie Mellon U, USA
A simplified account of the metatheory of linear LF