Unification in an extensional lambda calculus with ordered function sorts and constant overloading
From MaRDI portal
Publication:5210801
DOI10.1007/3-540-58156-1_45zbMath1433.68554OpenAlexW1515150570MaRDI QIDQ5210801
Michael Kohlhase, Patricia Johann
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
Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A modest model of records, inheritance, and bounded quantification
- A semantics of multiple inheritance
- A proof theory for general unification
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Computational aspects of an order-sorted logic with term declarations
- Higher-order order-sorted algebras
- Subtyping + extensionality: Confluence of βηtop reduction in F≤
- Unification in an extensional lambda calculus with ordered function sorts and constant overloading
This page was built for publication: Unification in an extensional lambda calculus with ordered function sorts and constant overloading
