## Stream: general

### Topic: Substructural type systems

#### Wojciech Nawrocki (Oct 31 2018 at 21:31):

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 (Nov 20 2018 at 05:52):

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 (Nov 20 2018 at 05:57):

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 (Nov 20 2018 at 05:57):

if you have tactic questions feel free to ask, though

#### Andrew Ashworth (Nov 20 2018 at 06:00):

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

#### Wojciech Nawrocki (Nov 20 2018 at 06:01):

Hm, how about inversion?

#### Andrew Ashworth (Nov 20 2018 at 06:02):

cases will do it

#### Mario Carneiro (Nov 20 2018 at 08:16):

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 (Nov 20 2018 at 16:26):

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).

Last updated: May 08 2021 at 10:12 UTC