System F is a typed lambda calculus that introduces universal quantification over types, forming the theoretical basis for languages such as Haskell and ML. It has variables ranging over terms and types, and binders for them. System F is strongly normalizing but type inference is undecidable. The "F" in System F was picked by chance.
University of Washington
Spring 2021
University of Washington's course develops rigorous tools to study the meaning of programs. It aims to improve formalism, proof skills, and precision in programming, while also discussing practical applications. It covers operational semantics, Hoare Logic, compiler correctness, and more.
No concepts data
+ 17 more concepts