Sciweavers

TLDI
2005
ACM
151views Formal Methods» more  TLDI 2005»
14 years 6 months ago
Strict bidirectional type checking
Completely annotated lambda terms (such as are arrived at via the straightforward encodings of various types from System F) contain much redundant type information. Consequently, ...
Adam J. Chlipala, Leaf Petersen, Robert Harper