A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
From MaRDI portal
Publication:5286030
DOI10.1142/S012905419200019XzbMATH Open0784.03013MaRDI QIDQ5286030FDOQ5286030
Authors: David Pym 
Publication date: 29 June 1993
Published in: International Journal of Foundations of Computer Science (Search for Journal in Brave)
Recommendations
- Higher-order unification with dependent function types
- Higher-order dynamic pattern unification for dependent types and records
- Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type
- Higher-order unification via combinators
- A higher-order unification algorithm for inductive types and dependent types
Cited In (16)
- Representing unification in a logical framework
- Delaying unification algorithms for lambda calculi
- Title not available (Why is that?)
- Higher-order dynamic pattern unification for dependent types and records
- The Alf proof editor and its proof engine
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- Equivalences between logics and their representing type theories
- Title not available (Why is that?)
- A note on the proof theory of the \(\lambda \Pi\)-calculus
- Reduction and unification in lambda calculi with a general notion of subtype
- Higher-order unification with dependent function types
- Proof-term synthesis on dependent-type systems via explicit substitutions
- Proof-search in type-theoretic languages: An introduction
- Title not available (Why is that?)
- An algorithm for checking incomplete proof objects in type theory with localization and unification
- The practice of logical frameworks
This page was built for publication: A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5286030)
