3 ms·
This is 100% false. The Calculus of Constructions is a superset of System F. You may be thinking of the fact that if you want your type system to be sound when
by taktoa 9y ago
This is 100% false. The Calculus of Constructions is a superset of System F. You may be thinking of the fact that if you want your type system to be sound when interpreted as a logic, then termination must be guaranteed (which would break backwards compatibility). Dependent types and totality are often found together, but are in actuality orthogonal features.