5 ms·
Multicore OCaml: October 2021
- natded 5y agoLinearly typed Ocaml /when/
- andreypopp 5y agoSee "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.
- pjmlp 5y agoThe "What is an Operating System?" podcast episode with Anil Madhavapeddy about MirageOS also discusses OCaml 5.0: https://signalsandthreads.com/what-is-an-operating-system/ https://signalsandthreads.com/what-is-an-operating-system/
- natded 5y agoThis is the only podcast I've ever bothered to listen to, its quite amazing (mean the series, but this particular one was very informative about unikernels)
- sydthrowaway 5y agoIf only colesbury joined Jane Street instead of FB
- devmunchies 5y agoso is the Tezos blockchain officially supported by the ocaml team?