This directory contains the correctness proofs for the type inferencer: both soundness and completeness proofs.
envRelScript.sml: Relating inference and type system environments.
inferCompleteScript.sml: Proves completeness of the type inferencer, i.e. if there is a type for the program, then the type inferencer will find a type (the most general type).
inferSoundScript.sml: Proves soundness of the type inferencer: any type assignment produced by the type inferencer is a valid type for the program.
infer_eCompleteScript.sml: Prove completeness of the type inferencer for the expression-level.
infer_eSoundScript.sml: Prove soundness of the type inferencer for the expression-level.
type_dCanonScript.sml: For any type_d, prove that the canonical type identifier strategy succeeds.
type_eDetermScript.sml: Prove determinism lemmas about the type inferencer.