-
Notifications
You must be signed in to change notification settings - Fork 0
Spring 2020
Monday 9:30-10:30 AM @ Google.Meet
Finished and took a break on Weeks of May 11th and 18th. See Summer-2020 for what follows.
Summary:
-
Awodey's book, Chap. 1, exercises 1–2.
-
Max's exercise about decidability of free categories.
Present: Artem, Cameron, Julia, Kartik, Olek
Summary: Finished Section 1.7 of Steven Awodey's book (free monoids and free categories). Plan to finish Ch-1 (1.8 about set-theoretic concerns, which may be not so much relevant to us) and do the exercises for Ch. 1 next time.
Steven Awodey's video lectures from OPLSS 2012 are available online and might be a good supplement.
Present: Alexi, Artem, Cameron, Ellen, Julia, Kartik
Summary: we started discussing free monoids (Section 1.7 of Steven Awodey's book) but haven't finished.
Next meeting: chapter 1 of Steven Awodey's book; we'll start with finishing section 1.7, and move on from there.
Present: Alexi, Artem, Cameron, Ellen, Julia, Kartik, Max, Olek
Summary: we discussed isomorphisms (Section 1.5 of Steven Awodey's book) and constructions on categories (Section 1.6).
Next meeting: chapter 1 of Steven Awodey's book; we'll start with finishing section 1.6, and move on from there.
Present: Alexi, Artem, Cameron, Ellen, Julia, Olek
Summary: we discussed examples of categories and non-categories from section 1.4 of Steven Awodey's book.
Next meeting: finish chapter 1 of Steven Awodey's book; we'll start with discussing section 1.5 on isomorphisms.
Present: Alexi, Artem, Ellen, Julia, Max, Olek
Outcomes
To prepare for the next meeting, read sections 1.1 – 1.5 of Steven Awodey's book (as usual, if you don't, come anyway — we'll go through the material anyway).
Details
-
We should decide if we want a general introduction or more CS/PL-related one. The people who spoke out seem to lean towards the latter.
-
Alternatives for the (text)books discussed
-
Emily Reihl's book — Olek has experience with it: seems more on the Math side of things (no apparent PL-related topics/examples covered), assumes some familiarity with abstract algebra (groups). Max suggests taking a look at Chapter 2 when it comes to it.
-
Awodey's book — Artem has experience with it: assumes some familiarity with abstract algebra (monoids), has PL-related examples (STLC), most gentle introduction from what was discussed, it seems. We decided to start with it.
-
Max suggested two sets of lecture notes that might be more useful for a PL researcher (semanticist), but which seem deeper and might be worth looking at a little bit later in the course:
-
Edward Morehouse's OPLSS notes from 2015 or 2016 (the two seem very similar).
-
Michael Shulman: Categorical logic from a categorical point of view — especially Chap. 0.
We will keep in touch with Max in the hope that he helps us to transition to these more advanced sources gradually.
Skipped due to general confusion about the virus and stuff.
-
Listened to ~2/3 of the POPL talk on Incorrectness logic — a nice summary of the main idea, not very smooth in explaining the technical details.
-
Dove into Condorcet voting a little bit and decided to follow up with yet another poll to chose the topic between the two main contenders, Agda and Category Theory.
Postmortem:
-
We went through sections 3 and ~half of 4, including a good portion of proof system rules from Fig. 2 and 3 in Section 4.
-
Next time: wrap up with Incorrectness logic by watching the POPL talk. Decide what to do next. Two main options are:
- Agda book (PLFA),
- Category theory.
Postmortem:
-
We went through sections 1 and 2. Started 3.1 and discussed the first example there.
-
Next time: we are going to continue.
To prepare:
Possible Topics
- Probabilistic Programming (sources?)
- Agda (Wadler's and others PLFA book, Conor McBride's lectures)
- (Algebraic) Effects & Extensible Effects (Cartwright & Felleisen, Oleg Kiselev, Andrej Bauer)
- Category Theory (Steve Awodey, Basic Category Theory, Emily Riehl)
- Functional Reactive Programming
- Subtyping (?)
- Quantum Computing/Programming (Robert Rand, quantum.country, Selinger Quantum lambda-calculus).
Random Good Papers
- Scheme papers by Guy Steele
- Cardelli's tail recursion
- Does Blame Shifting Work? (POPL 2020)
- Incorrectness logics (POPL 2020)
- On the expressive power of programming languages (talk by Shriram basing on Matthias' paper)
Rejected topics
- HCI/DataViz (which papers?)