Meetings ☕️
Reading group on PL topics by graduate students and friends at UiB.
Recurrent UiB:
Åsmund
Friends:
2021
06.10 | Filling the homotopies in Sups Bool inline_formula not implemented S1 | -
06.07 | Funext theorem and Sups Bool inline_formula not implemented S1 | Jonathan Cubides
05.27 | Online ☕️
05.10 | Intro. to Cubical type theory | Jonathan Cubides
05.06 | Chapter 4 of Escardo's Topology of data types | Elisabeth Bonnevier
04.29 | Prop 3.16 and Sec 3.13 | Elisabeth Bonnevier
W15 04.15 | EPIT Summer School
04.12 | Briefly intro to OCaml | Emmanuel Arrighi
04.05 | Compact spaces and Overt space | Elisabeth Bonnevier
W14 04.05 | Påske!
04.01 | Instance arguments in Agda | Elisabeth Bonnevier
03.29 | Structural and well-founded induction | Jonathan Cubides
03.25 | Proving programs terminating in DTT | Jonathan Cubides
03.22 | Topology on data types | Elisabeth Bonnevier
03.18 | Formalizing the Mathematics of Arrays II in Coq | Benjamin Chetioui
03.15 | Intro to compact types I | Elisabeth Bonnevier
03.11 | Formalizing the Mathematics of Arrays in Coq | Benjamin Chetioui
03.08 | Product topology, Hausdorff and compactness | Tam Thanh Truong
3.04 | Sierpinski space and continuity in topology | Tam Thanh Truong
3.01 | A brief intro to point-set topology | Tam Thanh Truong
2.25 | More monad transformers | Maxime Augier
2.22 | Seemingly-impossible-functional's blog post | Elisabeth Bonnevier
2.18 | ReaderT monad transformer | Maxime Augier
2.15 | Co-algebras and co-induction | Elisabeth Bonnevier
2.11 | F-algebras and initial algebras | Elisabeth Bonnevier
2.08 | inline_formula not implemented-calculus: Bisimulation | Jonathan Cubides
2.04 | Monads recap | Maxime Augier
2.01 | inline_formula not implemented-calculus: More | Jonathan Cubides
1.28 | Monad transformers in Haskell | Maxime Augier
1.21 | More on lenses in Haskell | Maxime Augier
1.18 | inline_formula not implemented-calculus: properties of STLC: preserve and proofs | Jonathan Cubides
1.14 | Lenses in Haskell | Maxime Augier
2020
12.18 | End for this year, Goodbye 2020
12.16 | Free session topic
12.11 | inline_formula not implemented-calculus: progress and proofs | Jonathan Cubides
12.09 | Substitution variable Monad | Håkon R. Gylterud
12.04 | inline_formula not implemented-calculus: recursion, call-by-value, Y-combinator | Jonathan Cubides
12.02 | inline_formula not implemented-calculus: syntax, (inline_formula not implemented-, inline_formula not implemented-, inline_formula not implemented-) relations, subst. | Jonathan Cubides
11.27 | Traversable and Foldable typeclasses in Haskell | Knut Anders
11.25 | Traversable types | Knut Anders ( overlapped the writing workshop)
11.20 | Functors, natural transf. and monads in Agda | Elisabeth Bonnevier
11.18 | Functors in Haskell | Knut Anders
11.13 | J2 | Folding and traversing data | Knut Anders
11.11| J2 | Monoids and lemmas | Tam Thanh Truong
11.06| J2 | Tail recursion optimization and higher-order functions | Knut Anders
11.04| J2 | Lists and higher-order functions | Knut Anders
10.30 | J2 | Decision procedures | Jonathan Cubides
10.28 | J2 | Propositions as types | Elisabeth Bonnevier
10.23| J2 | Martin-Löf type theory | Jonathan Cubides
10.21 | J2| Iso, Function extensionality and univalence | Elisabeth Bonnevier
10.16 | J1 | Encode-decode method | Jonathan Cubides
10.13 | J1 | Inductive definition of relations | Jonathan Cubides
10.11 | J1 | Rewriting and equational reasoning | Jonathan Cubides
10.09 | J1 | Equality | Jonathan Cubides
10.06 | J1 | Induction | Jonathan Cubides
10.03 | J1 | Naturals | Jonathan Cubides
09.29 | J1 | Agda introduction | Jonathan Cubides