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