5. CADE 1980:
Les Arcs, France
, Bob Welham
: Using Meta-Level Inference for Selective Application of Multiple Rewrite Rules in Algebraic Manipulation.
: Proofs as Description of Computation.
: A System for Proving Equivalences of Recursive Programs.
Paul Y. Gloess
: An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions.
: An Approach to Theorem Proving on the Basis of a Typed Lambda-Calculus.
: A Note on Resolution: How to Get Rid of Factoring without Loosing Completeness.
: Analysis of Dependencies to Improve the Behaviour of Logic Programs.
: Deciding Unique Termination of Permutative Rewriting Systems: Choose Your Term Algebra Carefully.
Joseph A. Goguen
: How to Prove Algebraic Inductive Hypotheses Without Induction.