With respect to keeping the language small and simple (C2x charter 6c
and 11) this of course adds a feature. It allows higher-order type
rules (Forall types X, T<X> is a type) which adds to C the remaining
part of the negative fragment of natural deduction for minimal logic
[1], implications being function types and conjunctions implemented
by struct types.
[1]
https://lipn.univ-paris13.fr/~mazza/teaching/ProofTheoryNotes.pdf
Sysop: | Keyop |
---|---|
Location: | Huddersfield, West Yorkshire, UK |
Users: | 248 |
Nodes: | 16 (2 / 14) |
Uptime: | 41:26:35 |
Calls: | 5,495 |
Calls today: | 3 |
Files: | 11,665 |
Messages: | 5,039,702 |
Posted today: | 2 |