Substructural type systems

Stream: general

[Wojciech Nawrocki]

Has anyone looked at or is familiar with Lean formalisations of substructural type systems (like linear types whose instances have to be used exactly once)?

[Wojciech Nawrocki]

If not that, perhaps someone has tried at least the base stuff like progress and preservation for simply-typed lambda calculus? I'm trying to follow Programming Language Foundations, except using de Brujin indices, but struggling a bit with the different Coq vs. Lean tactics.

[Andrew Ashworth]

Ah, I know a contributor to Rust posted here once asking about linear types, but unfortunately I don't think they are an active member of this chat room

[Andrew Ashworth]

if you have tactic questions feel free to ask, though

[Andrew Ashworth]

although, looking over PLF, I don't know a good replacement for eapply and friends

[Wojciech Nawrocki]

Hm, how about inversion?

[Andrew Ashworth]

cases will do it

[Mario Carneiro]

I think @Floris van Doorn did some work with PTSs in lean, and he is currently working on model theory for first order logic using de bruijn indices. I don't know how much of his stuff is available or applicable to you though

[Floris van Doorn]

I have not done PTSs in Lean, but in Coq only: http://florisvandoorn.com/ptsf/index.html
I'm now indeed working on first-order logic in Lean also using de Bruijn variables: https://github.com/flypitch/flypitch/blob/master/src/fol.lean
First-order logic is a bit simpler than lambda calculus, but the bookkeeping with de Bruijn variables is the same (search for lift_term_at, lift_formula_at, subst_term and subst_formula and their properties).