A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
From MaRDI portal
Publication:5286030
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)- The practice of logical frameworks
- Representing unification in a logical framework
- Delaying unification algorithms for lambda calculi
- scientific article; zbMATH DE number 1303341 (Why is no real title available?)
- 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
- scientific article; zbMATH DE number 1420794 (Why is no real title available?)
- A note on the proof theory of the -calculus
- Reduction and unification in lambda calculi with a general notion of subtype
- Higher-order unification with dependent function types
- Proof-search in type-theoretic languages: An introduction
- Proof-term synthesis on dependent-type systems via explicit substitutions
- scientific article; zbMATH DE number 3997190 (Why is no real title available?)
- An algorithm for checking incomplete proof objects in type theory with localization and unification
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)
