3 ms·
See "Kindly Bent to Free Us" https://dl.acm.org/doi/pdf/10.1145/3408985 https://dl.acm.org/doi/pdf/10.1145/3408985
by andreypopp 5y ago
See "Kindly Bent to Free Us"
https://dl.acm.org/doi/pdf/10.1145/3408985 https://dl.acm.org/doi/pdf/10.1145/3408985
- natded 5y agoWow, thank you for the link, looks very interesting from abstract.
- Drup 5y agoI'm the author if anyone has questions. :)
- Zababa 5y agoI 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 agoLinear 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.