Zulip Chat Archive

Stream: general

Topic: Substructural type systems


view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Andrew Ashworth (Nov 20 2018 at 05:57):

if you have tactic questions feel free to ask, though

view this post on Zulip Andrew Ashworth (Nov 20 2018 at 06:00):

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

view this post on Zulip Wojciech Nawrocki (Nov 20 2018 at 06:01):

Hm, how about inversion?

view this post on Zulip Andrew Ashworth (Nov 20 2018 at 06:02):

cases will do it

view this post on Zulip 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

view this post on Zulip 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