Eigenschaften polym. Typsyst.

• Termination:

  getypte Programme terminieren

• Rekonstruktion:

  es gibt Algorithmus, der Typ eines ungetypten Programms ausrechnet oder ablehnt, falls es keinen Typ besitzt

  (Rang 2: ja, beliebiger Rang: nein)