Course conclusion
Table of Contents
1. Metacognition
This is a google slides presentations that reflects on the independent study.
1.1. Slides: Why should you do an independendent study?
1.2. Things that could have been done better
Consistency
I found that some weeks I would work much less than on other weeks. Consistency would be nice because you learn better that way, and also allows you to maintain a good pace.
Plan asides
I suddenly got interested with proof theory and category theory. It wasn’t explicitly part of the syllabus. Maybe some planning for these would be been good, but I’m not too unhappy about how it went.
Have more meetings earlier
The 2 times a week pace felt better than 1 times a week. I don’t think it would strictly be better to meet 1 times a week early on, but it did become better for me when me and my advisor met more frequently.
2. LF
The majority of the work was in reading Logical Foundations and completing the exercises. The most important parts to learn about was proof by induction, tactics, the distinction between Prop and Bool, the Curry-Howard isomorphism, inductive propositions, and more sophisticated tactics. We skipped Imp.v, it was too similar to 15-316’s structural operational semantics and 15-312. We did most of the exercises, including advanced ones.
3. PLF
We had to skim this book heavily. We would have wanted to spend more time in PLF, as apparently, the exercises are less trivial, but LF is already incredibly huge. We may revisit this on our own as a companion to OPLSS (a seminar on Programming Language Theory) or 15312.
4. Category theory aside
It was nice to learn about category theory, even if just by scratching the surface. I learned about categories, universal constructions, and had a very quick, blurry glance of “internal logic”, “categorical logic”, “categorical semantics”, “topos theory” and “homotopy type theory”.
4.1. Slides: Badly organized notes
4.2. Lists of resources
5. Proof theory
5.1. Slides: Notes
https://docs.google.com/presentation/d/1Up7E6bG2ElCI2hodNyO1DMrA6Ck29nkIAMda_0Fma0w/edit?usp=sharing We made a huge (unpolished) slide deck for proof theory, it includes notes the philosophy and history of proof theory, notes on “the other kind of proof theory” - with an aside discusing the Hydra Game, and notes on structural proof theory - philosophy, metatheorems, proof systems, and considerations when formalizing proof systems in an ITP. The end includes schools on proof theory and educational resources.
6. Project
During the independent study, we applied for QSIURP as well. This entailed writing a proposal, literature review, and a presentation. We got accepted and will continue the work in the summer. It is about context representations of proof systems in Rocq.
6.1. Slides
7. Calendar for future work
End of semester: May 5 QSIURP: May 13-Aug 4 OPLSS: June 22-July 6