Project Page
Index
Table of Contents
SysF_PTS.Decidable
SysF_PTS.lib
SysF_PTS.sysf
Traditional, 2-sorted System F with explicits type variable contexts, a la Harper
Syntax
Type System
Internalising contexts
SysF_PTS.lambda2
Singel sorted PTS Lambda2
Syntax
System L - the usual PTS typing rules (without conversion)
System P - the auxilary type system
Better theory for L, exploiting LP Equivalence.
Internalising contexts
SysF_PTS.RelEquiv
Equivalence of F and Lambda2 - Using relations
Relating Types
Relating terms