On Irrelevance and Algorithmic Equality in Predicative Type Theory

DOI10.2168/LMCS-8(1:29)2012zbMath1238.03028arXiv1203.4716MaRDI QIDQ2881097

Gabriel Scherer, Andreas Abel

Publication date: 3 April 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1203.4716

zbMATH Keywords

dependent typeslogical relationproof irrelevancetyped algorithm equalityuniversal Kripke model

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Equality Checking for General Type Theories in Andromeda 2, Canonicity and normalization for dependent type theory, POPLMark reloaded: Mechanizing proofs by logical relations, A dependent dependency calculus, An extensible equality checking algorithm for dependent type theories, Unnamed Item, Graded modal dependent type theory, Is Impredicativity Implicitly Implicit, Unnamed Item, Mechanizing proofs with logical relations – Kripke-style, An adequacy theorem for dependent type theory, Canonicity for cubical type theory, Unnamed Item

Uses Software

• Coq
• Cayenne
• Agda