A higher-order unification algorithm for inductive types and dependent types

DOI10.1007/BF02948973zbMath0878.68069MaRDI QIDQ1362142

Qingping Tan

Publication date: 1997

Published in: Journal of Computer Science and Technology (Search for Journal in Brave)

zbMATH Keywords

higher-order logiclambda calculusinductive typeslogical framework

Mathematics Subject Classification ID

Parallel algorithms in computer science (68W10)

Cites Work

• A unification algorithm for typed \(\overline\lambda\)-calculus
• Mechanizing \(\omega\)-order type theory through unification
• A framework for defining logics

This page was built for publication: A higher-order unification algorithm for inductive types and dependent types