Go backward to Points and Tiles Go up to Top Go forward to References

Summary

• Three main principles
  • Universal type quantification (polymorphism).
  • Existential type quantification (abstraction).
  • Bounded type quantification (subtyping).
• Resulting programs may be statically type-checked.
  • Bottom-construction of types.
  • More sophisticated type inference possible (ML).
• More general type systems.
  • Type-checking typically not decidable any more.
  • Dependent types (Martin-Löf).
  • Calculus of constructions (Coquand and Huet)..