Unification in an extensional lambda calculus with ordered function sorts and constant overloading

DOI10.1007/3-540-58156-1_45MaRDI QIDQ5210801zbMATH OpenOpenAlexFDO

Authors Patricia Johann, Michael Kohlhase

Publication date 21 January 2020

Published in Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL http://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/352

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 1324447
• Higher-order unification, polymorphism, and subsorts
• Higher-order unification with dependent function types
• Computational aspects of an order-sorted logic with term declarations
• Order-sorted unification

Cites work

• A modest model of records, inheritance, and bounded quantification
• A proof theory for general unification
• A semantics of multiple inheritance
• A unification algorithm for typed -calculus
• Computational aspects of an order-sorted logic with term declarations
• Higher-order order-sorted algebras
• scientific article; zbMATH DE number 1324447 (Why is no real title available?)
• scientific article; zbMATH DE number 1348466 (Why is no real title available?)
• scientific article; zbMATH DE number 575379 (Why is no real title available?)
• Subtyping + extensionality: confluence of \(\beta \eta\)top reduction in \(\mathrm{F}_\leq\)
• Unification in an extensional lambda calculus with ordered function sorts and constant overloading

Cited in

(6)

• scientific article; zbMATH DE number 1303341 (Why is no real title available?)
• scientific article; zbMATH DE number 1324447 (Why is no real title available?)
• scientific article; zbMATH DE number 3997190 (Why is no real title available?)
• Higher-order unification with dependent function types
• Unification in an extensional lambda calculus with ordered function sorts and constant overloading
• Higher-order unification, polymorphism, and subsorts

This page was built for publication: Unification in an extensional lambda calculus with ordered function sorts and constant overloading

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