Abstract is missing.
- The Hydra Battle RevisitedNachum Dershowitz, Georg Moser. 1-27 [doi]
- Orderings and Constraints: Theory and Practice of Proving TerminationCristina Borralleras, Albert Rubio. 28-43 [doi]
- Narrowing, Abstraction and Constraints for Proving Properties of Reduction RelationsIsabelle Gnaedig, Hélène Kirchner. 44-67 [doi]
- Computability Closure: Ten Years LaterFrédéric Blanqui. 68-88 [doi]
- Reduction Strategies and AcyclicityJan Willem Klop, Vincent van Oostrom, Femke van Raamsdonk. 89-112 [doi]
- Towards Rewriting in CoqJacek Chrzaszcz, Daria Walukiewicz-Chrzaszcz. 113-131 [doi]
- Superdeduction at WorkPaul Brauner, Clément Houtmann, Claude Kirchner. 132-166 [doi]
- Remarks on Semantic Completeness for Proof-Terms with Laird s Dual Affine/Intuitionistic ::::lambda:::: -CalculusMitsuhiro Okada, Ryo Takemura. 167-181 [doi]
- Linear Recursive FunctionsSandra Alves, Maribel Fernández, Mário Florido, Ian Mackie. 182-195 [doi]
- Deducibility Constraints, Equational Theory and Electronic MoneySergiu Bursuc, Hubert Comon-Lundh, Stéphanie Delaune. 196-212 [doi]
- Applying a Theorem Prover to the Verification of Optimistic Replication AlgorithmsAbdessamad Imine, Michaël Rusinowitch. 213-234 [doi]
- Towards Modular Algebraic Specifications for Pointer Programs: A Case StudyClaude Marché. 235-258 [doi]
- Modeling Permutations in Coqfor CoccinelleEvelyne Contejean. 259-269 [doi]