A Complete Mechanization of Second-Order Type Theory

DOI10.1145/321752.321764zbMATH Open0253.68021OpenAlexW2140669384MaRDI QIDQ5667481FDOQ5667481

Authors Tomasz Pietrzykowski

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

Mathematics Subject Classification ID

Proof theory and constructive mathematics (03F99)

Cited in

(16)

• A compact representation of proofs
• On the undecidability of second-order unification
• Decidability of the unification problem for second-order languages with unary functional symbols
• Interpretation and inference with maximal referential terms
• Steps toward a computational metaphysics
• Higher-order unification via combinators
• Mechanizing \(\omega\)-order type theory through unification
• Linear second-order unification
• A unification algorithm for typed \(\overline\lambda\)-calculus
• On equality up-to constraints over finite trees, context unification, and one-step rewriting
• Unification under a mixed prefix
• A unification algorithm for typed \(\bar\lambda\)-calculus
• lambda-normal forms in an intensional logic for English
• A decision algorithm for distributive unification
• A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
• Higher-order unification revisited: Complete sets of transformations

Describes a project that uses

Uses Software

• Automath

This page was built for publication: A Complete Mechanization of Second-Order Type Theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5667481)