This program is tentative and subject to change.
We introduce ghost type theory (GTT) a dependent type theory extended with a new universe for ghost data that can safely be erased when running a program but which is not proof irrelevant like with a universe of (strict) propositions. Instead, ghost data carry information that can be used in proofs or to discard impossible cases in relevant computations. Casts can be used to replace ghost values by others that are propositionally equal, but crucially these casts can safely be ignored for conversion. We provide a type-preserving erasure procedure which gets rid of all ghost data and proofs, a step which may be used as a first step to program extraction. We give a syntactical model of GTT using a program translation akin to the parametricity translation and thus show consistency of the theory. Because it is a parametricity model, it can also be used to derive free theorems about programs using ghost code. We further extend GTT to support equality reflection and show that we can eliminate its use without the need for the usual extra axioms of function extensionality and uniqueness of identity proofs. In particular we validate the intuition that indices of inductive types—such as the length index of vectors—do not matter for computation and can safely be considered modulo theory. The results of the paper have been formalised in Coq.
This program is tentative and subject to change.
Tue 3 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | Type TheoryICFP Papers and Events / JFP First Papers | ||
13:30 18mTalk | Normalization by evaluation for modal dependent type theoryJFP First Paper JFP First Papers Jason Z.S. Hu McGill University, Junyoung Jang McGill University, Brigitte Pientka McGill University DOI | ||
13:48 18mTalk | Closure-Free Functional Programming in a Two-Level Type Theory ICFP Papers and Events András Kovács University of Gothenburg DOI Pre-print | ||
14:06 18mTalk | Gradual Indexed Inductive Types ICFP Papers and Events Mara Malewski Correa University of Chile, Chile, Kenji Maillard Inria, Nicolas Tabareau Inria, Éric Tanter University of Chile | ||
14:24 18mTalk | Dependent Ghosts Have a Reflection for Free ICFP Papers and Events Theo Winterhalter INRIA Saclay | ||
14:42 18mTalk | Static Blame for gradual typingJFP First Paper JFP First Papers Chenghao Su Nanjing University, Lin Chen Nanjing University, Yanhui Li Nanjing University, Yuming Zhou Nanjing University DOI |