A Complete Mechanization of Second-Order Type Theory
From MaRDI portal
Publication:5667481
DOI10.1145/321752.321764zbMath0253.68021OpenAlexW2140669384MaRDI 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
Related Items
Higher-order unification via combinators, Linear second-order unification, A compact representation of proofs, Steps toward a computational metaphysics, lambda-normal forms in an intensional logic for English, Unification under a mixed prefix, Interpretation and inference with maximal referential terms, A unification algorithm for typed \(\bar\lambda\)-calculus, A unification algorithm for typed \(\overline\lambda\)-calculus, Mechanizing \(\omega\)-order type theory through unification, Decidability of the unification problem for second-order languages with unary functional symbols, A decision algorithm for distributive unification, Higher-order unification revisited: Complete sets of transformations, On equality up-to constraints over finite trees, context unification, and one-step rewriting, On the undecidability of second-order unification, A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
Uses Software
