-
Notifications
You must be signed in to change notification settings - Fork 0
Fall 2021
Fridays @ 1:00–2:00pm in Olek's Zoom
We are going through PLFA. 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.
Attendees: Olek, Artem, Julia, John Li, Cameron
Summary: We stepped in detail through *-comm trying to write out the proof
term explicitly instead of using rewriting or the long form equational
reasoning. We ended up using Eq.trans, which takes two proofs of equivalences
and composes them. We also found there are 5 explicit arguments, of which the
first two don't matter, but the last three are the three statements we use the
transitivity of equivalence on. Next time, we plan to start reading Relations.
Given the PLDI deadline is on 11/19, I won't be able to make that meeting. Since Thanksgiving is the week after, our next meeting will be 12/3.
Homework: If you aren't caught up, complete the exercises in induction.
Attendees: Olek, Artem, Julia, Yangtian, John Li
Summary: We stepped through the following exercises: operators, +-swap, and *-distrib-+. While doing the exercises, we tried out both the equational reasoning and rewriting styles. We had heard that neither of those styles were often times used by more serious Agda programmers, so we took a look through the agda code base of the paper Leibniz Equality is Isomorphic to Martin-Lof Identity, Parametrically. We found that the code seemed to emphasize using "where" blocks to define helper functions.
Homework Finish the rest of the exercises in Induction: *-assoc, *-comm*, 0∸n≡0, ∸-|-assoc, +*^, and Bin-laws.
Attendees: Olek, Madkour, John Li, John Gouwar, Andrew
Summary: Note: we will not be meeting on 10/29 due to a seminar conflict. Our next meeting will be november 5th.
We stepped through the Bin exercise in Naturals, emphasizing the different editor commands that agda-mode in emacs provides. We finished reading through Induction.
Homework: Do the exercises in Induction (feel free to skip the creation story one).
Attendees: Olek, Artem, Julia, Madkour, Yangtian, Cameron, John Li, John Gouwar
Summary: We stepped through Naturals up until "Writing Definitions Interactively". We're going to start next time by reviewing the Bin exercise and then reading Induction.
Homework: Finish reading Naturals and do the Bin exercise.
Attendees: Olek, Andrew, Artem, Julia, Michelle, Yangtian, Cameron, John Li
Summary: We discussed the format, which I've added above. In short, we will alternate between reading and working through exercises, with a leader for each exercise session.
Homework: Get Agda installed. Read through and finish up exercises in Naturals.