Proving Properties About a Lazy Functional Language with the Coq Proof Development System

In this report, proofs of various properties of a deductively defined reduction system are presented. The reduction system is an operational semantics for a functional language implementing lazy evaluation, which is described by deductions. The properties proved include subject reduction and a characterization of normal forms. These proofs are mechanically verified using Coq, an interactive proof development system. This paper is the full version of the extended abstracts.