[andreypopp]

See "Kindly Bent to Free Us"

https://dl.acm.org/doi/pdf/10.1145/3408985

[Drup]

I'm the author if anyone has questions. :)

[Zababa]

I have a general question regarding type theory. I'd like to learn more about it to be able to read and understand papers like these. From what I've read, Types and Programming Languages by Benjamin C. Pierce would be a good the place to start. Is this true? I don't see any mention of linear types in it, is this something you learn by reading papers?

[natded]

Linear Types are fairly new thing, you can read about them in constructivist logic (under the subset of 'linear logic', or 'resource-aware logic' or from newer type theory stuff under 'linear types').

I would recommend reading Harper's PFPL: https://www.cs.cmu.edu/~rwh/pfpl.html

OPLSS also has lots of videos about programming language theory and application, and the 2021 has a lecture series from Harper, introducing the topic:

https://www.cs.uoregon.edu/research/summerschool/summer21/to...

Couple resources I've used for type theory:

- https://www.andrew.cmu.edu/course/15-312/schedule.html

- http://cs.brown.edu/courses/cs173/2012/book/

- https://web2.qatar.cmu.edu/cs/15312/#schedule

- https://www.cs.cornell.edu/courses/cs4110/2020fa/schedule.ht...

- https://www.cs.cornell.edu/courses/cs6110/2019sp/schedule.ht...

- https://student.cs.uwaterloo.ca/~cs442/W21/notes/

More technical introductions to type theory:

- with AGDA: plfa.github.io

- with COQ: https://softwarefoundations.cis.upenn.edu

- with Lean: https://leanprover.github.io/theorem_proving_in_lean4/title_...

Constructivist Logic

- https://symbolaris.com/course/constlog-schedule.html

- https://github.com/michaelt/martin-lof - Recommend starting with the 1983 paper on logical constants.

[Zababa]

Thank you for all these resources!

[natded]

No problem, I enjoy reading about type theory and trying to apply them in practical programming as a hobby.

[natded]

Wow, thank you for the link, looks very interesting from abstract.