A complete mechanization of second-order type theory. (English) Zbl 0253.68021
MSC:
68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
03F99 | Proof theory and constructive mathematics |
03B15 | Higher-order logic; type theory (MSC2010) |
68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
03F99 | Proof theory and constructive mathematics |
03B15 | Higher-order logic; type theory (MSC2010) |