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

DOI10.1007/3-540-61780-9_70MaRDI QIDQ4647580zbMATH OpenOpenAlexFDO

Authors 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 assistanttype checktype conversiontyping ruleunification algorithm

Mathematics Subject Classification ID

Recommendations

• On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
• A partial type checking algorithm for Type:Type
• A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
• A modular type-checking algorithm for type theory with singleton types and proof irrelevance
• scientific article; zbMATH DE number 65534

Cites work

• A Complete Proof Synthesis Method for the Cube of Type Systems
• A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Higher-order unification with dependent function types
• scientific article; zbMATH DE number 65534 (Why is no real title available?)
• scientific article; zbMATH DE number 512787 (Why is no real title available?)
• Introduction to generalized type systems

Cited in

(1)

• A new refinement type system for automated \(\nu\text{HFL}_\mathbb{Z}\) validity checking

Describes a project that uses

Uses Software

• ALF

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4647580)