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

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 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/topics.php 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 https://www.andrew.cmu.edu/course/15-312/schedule.html - http://cs.brown.edu/courses/cs173/2012/book/ http://cs.brown.edu/courses/cs173/2012/book/ - https://web2.qatar.cmu.edu/cs/15312/#schedule https://web2.qatar.cmu.edu/cs/15312/#schedule - https://www.cs.cornell.edu/courses/cs4110/2020fa/schedule.html https://www.cs.cornell.edu/courses/cs4110/2020fa/schedule.ht... - https://www.cs.cornell.edu/courses/cs6110/2019sp/schedule.html https://www.cs.cornell.edu/courses/cs6110/2019sp/schedule.ht... - https://student.cs.uwaterloo.ca/~cs442/W21/notes/ 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 https://softwarefoundations.cis.upenn.edu - with Lean: https://leanprover.github.io/theorem_proving_in_lean4/title_page.html https://leanprover.github.io/theorem_proving_in_lean4/title_... Constructivist Logic - https://symbolaris.com/course/constlog-schedule.html https://symbolaris.com/course/constlog-schedule.html - https://github.com/michaelt/martin-lof https://github.com/michaelt/martin-lof - Recommend starting with the 1983 paper on logical constants.