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

DOI10.1007/3-540-61780-9_70zbMATH Open1407.68438OpenAlexW1534130495MaRDI QIDQ4647580FDOQ4647580

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

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

zbMATH Keywords

proof assistantunification algorithmtype conversiontype checktyping rule

Mathematics Subject Classification ID

Cites Work

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

Cited In (1)

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

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)