- (Term abhängig von Term, Funktion auf Daten)
- Typ abhängig von Typ (Typkonstruktoren: Functor, Monad)
- Term abhängig von Typ (System F)
- Typ abhängig von Term (dependent Types: Coq, PVS, ...)
(der Lambda-Würfel, Barendregt 1991)
http://www.cs.ru.nl/~henk/
2009-11-20
