A Complete Mechanization of Second-Order Type Theory
From MaRDI portal
Publication:5667481
DOI10.1145/321752.321764zbMath0253.68021MaRDI QIDQ5667481
Publication date: 1973
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/321752.321764
03F99: Proof theory and constructive mathematics
Related Items
Unification under a mixed prefix, A unification algorithm for typed \(\bar\lambda\)-calculus, A unification algorithm for typed \(\overline\lambda\)-calculus, Mechanizing \(\omega\)-order type theory through unification, A decision algorithm for distributive unification, On the undecidability of second-order unification, Higher-order unification via combinators
Uses Software