4 ms·

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

by Drup 5y ago

Zababa 5y ago
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 5y ago
  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.
  - Zababa 5y ago
    Thank you for all these resources!
    - natded 5y ago
      No problem, I enjoy reading about type theory and trying to apply them in practical programming as a hobby.

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

by Drup 5y ago

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

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 5y ago
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.
- Zababa 5y ago
  Thank you for all these resources!
  - natded 5y ago
    No problem, I enjoy reading about type theory and trying to apply them in practical programming as a hobby.