Formalizing equational reasoning in proof systems based on type theory
Eric Barendsen, University of Nijmegen, The Netherlands
Abstract:
Typed lambda calculus is an attractive basis for machine-assisted proof
development: representing derivations as syntactic objects (lambda terms)
enables easy manipulation and communication of proofs.
Formalization of equational reasoning in type theory turns out to be
problematic: straightforward axiomatization of equational logic gives rise
to tedious proofs. In this talk we will discuss some efficient
alternatives in which proofs are replaced by computations.