/sn-stlc-de-bruijn-coq

Strong Normalization for Simply-Typed Lambda-Calculus with de Bruijn indices in Coq

Primary LanguageCoq

Enclosed is a proof of strong normalization (SN) for simply-typed
lambda-calculus (STLC) in Coq using de Bruijn indices. It uses the Tait-Girard
technique of a "Reducibility" predicate which is recursive on the type. I
believe it to be the smallest direct proof of that fact using those methods
(i.e. de Bruijn indices in Coq), although the one by Adam Koprowski, part of
the CoLoR library, is elegant and more general.

See sn.pdf for more description, or start reading the Coq code at sn3.v.