-
Notifications
You must be signed in to change notification settings - Fork 0
Spring 2022
Mondays @ 2:00–3:00pm in Olek's Zoom
Starting 5/2/22, we are now working on formalizing various PL concepts in Agda, using this shared repo.
Here's the old plan we were following: We are continuing through PLFA. Similar to last semester, we will aim to alternate weeks between interactively reading through a chapter and doing exercises. We hope to have a leader for each exercise session to run through the problems.
- "C-c C-." - "agda2-goal-and-context-and-inferred": Goal type, context and inferred type
- "M-." - "agda2-goto-definition-keyboard": Go to definition of identifier under point
- "C-x C-u =" - "describe-char": put your cursor on a symbol to get information about it
Attendees: Olek, Artem, John Li, Matt
Summary: We had a long chat about the future of PL Seminar Jr, and decided that we would continue our Agda reading group in a project focused manner. The long term goal would be to make a kind of public facing wiki for PL theory done in Agda, but in the short term we plan to collaboratively formalize examples.
The general structure will be that the formalizations are all opt-in, so there are no assignments. Every week, we keep the structure open ended: if anyone has something interesting they'd like to share, or a problem they'd like help with, they can use the meeting time for discussions/collaborative programming. Our default if no one has such a contribution is to collaboratively write a formalization for an example.
Today, we wrote a formalization for a small arithmetic language, and heavily made use of Agda's interesting notation to cleanly write a denotational semantics. We also rewrote the typing judgements as abstract syntax, and found typechecking was nice and immediate.
Homework: For future, we won't have any assigned homework, since formalization work is opt-in.
Attendees: Olek, Artem, John Li
Summary: We chatted a bit about the proof assistant stack exchange question from last week, and read through Connectives, where we stopped at Distribution.
Homework: ⊎-comm, ⊎-assoc, ⊥-identityl and ⊥-identityr.
Attendees: Olek, Artem, John Li
Summary: We went over the homework from last week, and found that based on the presence of curly braces in the lambdas, the goal generated by Agda for the "from composed with to" case of the isomorphism was different. We started exploring, and found we didn't really understand what a curly braces being there or not being there meant, and how it works with type inference. We posted our example and question on the proofassistants stack exchange here.
Homework: None for this week!
Attendees: Olek, Artem, John Li, Matt
Summary: We read through Connectives up before disjunction is sum. We noted just how fragile the constructor notation is here: spaces really matter! ⟨_,_⟩ is a function, ⟨ _ , _ ⟩ is a product, and ⟨_ ,_⟩ or any other variation is a syntax error. We also discussed how Agda seems to build in extra simplification for record types.
Homework: Do the exercise ⇔≃×
Attendees: Olek, Artem, John Li, Andrew
Summary: We finished reading Isomorphism, and the binary exercise (which was just copy and pasting from Induction and then constructing the record). Next time we will read Connectives. We read just the few first sentences, and discussed how you can nest and partially apply the tuple constructor.
Homework: None for this week!
Attendees: Olek, Artem, John Li, Matt
Summary: We finished reading Equality, and started reading Isomorphism up through Isomorphism. Next time we will continue reading with Isomorphism as an equivalence.
Homework: None for this week!
Attendees: Olek, Artem, John Li, Matt
Summary: We continued reading Equality, and got hung up on Rewriting Expanded. We spent a while examining how the multi pattern match worked. We spent part of the time reading through the McBride 2004 paper to see how with abstractions worked, and found the examples on page 20 somewhat informative. We also played around with some minimal examples, and found that the strategy for desugaring a with clause into a where defined helper function had some heuristics for argument ordering that weren't necessarily easy to follow. We failed to break these heuristics and convinced ourselves it would be hard to, assuming our understanding of how they work is correct!
Homework: None for this week!
Attendees: Olek, Artem, John Li, Matt
Summary: We started reading Equality, and got up to Multiple Rewrites.
Homework: Do <=-Reasoning if you're feeling particularly motivated.
Attendees: Olek, Artem, John Li
Summary: We worked through the trichotomy and o+o=e, exercises. We notably spent some time thinking about how to search for definitions, and found C-c C-z to be helpful for that. Next time, we will start reading Equality
Homework: Do the o+o=e and Bin-predicates exercises.
Attendees: Olek, Julia, Artem, John Li, Andrew
Summary: We worked through the *-mono-<=, <-trans, <=-iff-<, and <-trans-revisited exercises. Next time, we will go over the remaining homework and start reading Equality
Homework: Do the trichotomy and Bin-predicates exercises.
Attendees: Olek, Artem, Julia, John Li
Summary: We continued reading Relations up through the section Monotonicity.
Homework: Do the *-mono-<= exercise, and if you can, read through strict inequality and do the exercises there.
Attendees: Olek, Artem, Julia, John Li, Andrew
Summary: We read Relations up through the section Reflexivity, and collaboratively did the orderings exercise.
Homework: Review an exercise in Induction to refamiliarize yourself with keybindings. Naturals has a short list of useful keybindings, and the agda-mode doc has a much more in depth list.