2025/01/07 by Yiyun Liu, Jonathan Chan, Stephanie Weirich · 1 voice · 1 citation
Computer Science · #Logic, programming, and type systems #Computability, Logic, AI Algorithms #Logic, Reasoning, and Knowledge
paper · doi:10.1145/3704843
The Dependent Calculus of Indistinguishability (DCOI) uses dependency tracking to identify irrelevant arguments and uses indistinguishability during type conversion to enable proof irrelevance, supporting run-time and compile-time irrelevance with the same uniform mechanism. DCOI also internalizes reasoning about indistinguishability through the use of a propositional equality type indexed by an observer level. As DCOI is a pure type system, prior work establishes only its syntactic type safety, justifying its use as the basis for a programming language with dependent types. However, it was not clear whether any instance of this system would be suitable for use as a type theory for theorem proving. Here, we identify a suitable instance <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mrow> <mml:msup> <mml:mrow> <mml:mtext>DCOI</mml:mtext> </mml:mrow> <mml:mi>ω</mml:mi> </mml:msup> </mml:mrow> </mml:math> , which has an infinite predicative universe hierarchy. We show that <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mrow> <mml:msup> <mml:mrow> <mml:mtext>DCOI</mml:mtext> </mml:mrow> <mml:mi>ω</mml:mi> </mml:msup> </mml:mrow> </mml:math> is logically consistent, normalizing, and that type conversion is decidable. We have mechanized all results using the Coq proof assistant.