• People
• Events
• Research

Brewing Strong Normalization Proofs with LEGO

Abstract: This is the documentation of completely formalized normalization proofs for Church style presentations of simply typed Lambda Calculus and System F in LEGO. The underlying type theory is the Calculus of Constructions enriched by inductive types. The proofs follow Girard et al [GLT89] but we make essential use of general inductive types to simplify the presentation. I will use this example to discuss Computer Aided Formal Reasoning in general.

LFCS report ECS-LFCS-92-230