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