Had some unsettling but interesting research thoughts during a few-hour blackboard session early this afternoon. Unsettling because it makes me keep wanting to change the overall story I want to tell in my thesis. Right now it's looking like this:
We have a lot of experience encoding formal systems in LF, and encoding properties and proofs about these systems. Inductive proofs in particular are encoded as recursive logic programs, written as LF signatures. We have good techniques and tools for "meta-reasoning", verifying totality of such programs, and thereby correctness of the proofs they represent.
Now there's been considerable past work extending LF with substructural features, e.g. linear LF, ordered LF, concurrent LF. These frameworks are really nice for encoding systems that involve state, stack discipline, and concurrency, respectively. Of course there's nothing stopping us from tediously encoding these features in a more low-level way in LF, but it's, well, tedious. Turning the Curry-Howard crank on substructural logics to yield expressive substructural type systems is much more pleasant.
However, existing LF meta-reasoning techniques stall on its substructural extensions. It's not clear what programs to write to correspond to the theorems we ordinarily prove. The main thing I'd like to contribute is a solution to this problem. It's not a final answer, but it's a start; I can describe a language that has LLF and OLF as subsets, and in which I have a couple concrete examples of new theorems you can state and prove.
But here's the thing where I start wanting to change my story. This system above is LF with a modified judgment, three new types (A ::= ... | A@p | ↓α.A | ∀α.A) and one new kind (K ::= ... | Πα.K). Recently I noticed that if I don't care about a user-friendly embedding of LLF and OLF I can completely get rid of the types A@p and ↓α.A. They're just syntactic sugar that can be compiled away. In the absence of them, the funny new judgment is eliminable as well: I can just use the Π-world kind to index any type with a world "internally".
What's left is just LF with one new type and one new kind. Moreover, the new type is extremely suspiciously close to Frank's original and apparently buggy notion of proof irrelevant function type back in his 2001 paper. What's clear is that the functionality lemma isn't provable, but I'm beginning to wonder — despite believing until now that I completely put the issue to rest in my mind with my senior thesis — if the problem is the statement of the lemma, not the system it's about.
If my hunch is right, then there is a complete compilation path from a metatheory-supporting external language that extends LLF and OLF, all the way down to LF + proof irrelevance, in a way that preserves the operational semantics of proof search. I think that would be pretty cool if it all worked.