An Axiom free formalization of several lambda calculi.

Every Calculus in this Project has its own folder in theories.

For Simply Typed Lambda Calculus, look at the file in theories/Stlc in this order:

Stlc Term Step Confluence Relations Typing StrongNormalization Interpretation StrongNormalizationProof

SysF and CC pretty much have the same structure

Preservation in SysF has a single admit left somewhere, will be fixed at some point The strong norm proof for SysF is closed under global context regardless of this, as it does not depend on Preservation

Running make will compile stlc and sysf without errors, but will not fully compile everything in CC, as it is work in progress