An algorithm for checking incomplete proof objects in type theory with localization and unification

DOI10.1007/3-540-61780-9_70zbMath1407.68438OpenAlexW1534130495MaRDI QIDQ4647580

Lena Magnusson

Publication date: 15 January 2019

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61780-9_70

zbMATH Keywords

proof assistantunification algorithmtype conversiontype checktyping rule

Mathematics Subject Classification ID

Uses Software

• ALF

Cites Work

• A unification algorithm for typed \(\bar\lambda\)-calculus
• A Complete Proof Synthesis Method for the Cube of Type Systems
• Introduction to generalized type systems
• Higher-order unification with dependent function types
• A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
• Unnamed Item
• Unnamed Item

This page was built for publication: An algorithm for checking incomplete proof objects in type theory with localization and unification