Past Talks
Some of our past talks and abstracts are here.
Spring 2024
| Date | Speaker | Abstract |
|---|---|---|
| 1/22/2024 | James Wilson | Why Categories at all? (Denotational Semantics) |
| 1/29/2024 | William Scarbro, Jonathan Yallop | “After reviewing the Natural Numbers Game, we would like to build up to the quotient remainder theorem. Along the way we will cover: Basic Syntax, Currying, Induction, Tactics, The Church Rosser Property, Dependent Types, Existential Quantifiers as Dependent Pairs” |
| 2/5/2024 | Continued from last week | |
| 2/12/2024 | Amaury Miniño,Sam Scheuerman | Wrapping up the natural numbers stuff and then modus ponens/modus tolens proofs |
| 2/19/2024 | Amaury Miniño,Sam Scheuerman | Continued from last week |
| 2/26/2024 | Alex Karduna, Chris Liu | Division algorithm - computation and proofs all in one. |
| 3/4/2024 | James Wilson | Type Theory Bootcamp |
| 3/18/2024 | Entire group | Post spring break chat |
| 3/25/2024 | James Wilson | “TOPOS: How to code a set in a computer. Abstract: For a century math folk have been getting away with saying things like ``Let a prime is number with exactly two factors. For every prime p….’’. In the first sentence we behave as though primes are a membership test P(n); so, S = { n | P(n) }. In the second sentence we without explanation began to image primes are enumerated; so, S={2,3,5,…}. Obviously there is a computational gap in this change in behavior. Mathematicians a century ago sought to fill it in by axiom. TOPOS is the name given to one strategy to close the gap in a computationally meaningful way. This means that if we write down a set in a TOPOS way, it has the ingredients to link membership with enumeration. I will lay out the motives and describe the three pillars upon which TOPOS can be defined and in the coming weeks we can build these pillars in math and in code.” |
| 4/1/2024 | Jonathan | Lambda calculus/substitution/combinators |
| 4/8/2024 | Amaury, Jerett | Types & Diagrams in Simple Type Theory |
| 4/15/2024 | Alex Karduna, William | Product & Dependent Functions |
| 4/22/2024 | William, Chris | Dependent sums, and subset classifier |
| 4/29/2024 | Ian | Membership / Suboject classifier - defining a topos. |
Fall 2023
| Date | Speaker | Abstract |
|---|---|---|
| September 9, 2023 | Wolfgang Bangerth/James Wilson | Why think functional / Loops and Recursion |
| September 13, 2023 | Kylie Schnoor/Mason Faldet | Higher Order Functions |
| September 20, 2023 | Mason Faldet/Sarah Lutz | Polymorphism / Inductive types |
| October 4, 2023 | James Wilson | Categories, Types, and Programs: A quick tour of the math used in modern programs. |
| October 11, 2023 | Kristina Moen/Fernando Herrera Valverde | Trees and pattern matching |
| October 25, 2023 | Chris Liu | Option data type and my Sunday |
| November 1, 2023 | Chris Liu | Big tent of functional programming |
| November 8, 2023 | Wolfgang Bangerth | Option data type and exceptions |
| November 29, 2023 | Ian Jorquera | F-Algebras (Functor Algebras, not to be confused with ill feelings about algebra) and the fold map or just more Functors |
Spring 2023
| Date | Speaker | Abstract |
|---|---|---|
| January 24, 2023 | James Wilson | High level survey of Homotopy Type Theory |
| January 31, 2023 | Ian Jorquera Kylie Schnoor |
Simple Types: $A \times B$ and $f: A \rightarrow B$ |
| Februart 7, 2023 | James Wilson | Combinators in different programming languages |
| February 14, 2023 | Chris Liu Kristina Moen |
Dependent Types: $\prod_{i \in I}A_i$ and $\coprod_{i \in I}A_i$ |
| February 20, 2023 | Emily Riehl | Title: Homotopy type theory and univalent foundations Abstract: This talk will introduce alternative foundations for mathematics in which “equality” becomes “identity,” which is no longer a mere predicate but can carry structure. The primitive notion is called a “type,” which can be interpreted as something like a set, or as something like a mathematical proposition, as a something like a groupoid or moduli space, which has higher structure. What Voevodsky named the “univalent foundations of mathematics” arose from a recently discovered homotopy theoretic interpretation of dependent type theory, originally designed as a formal system for constructive mathematics. We will introduce this formal system, explore Voevodsky’s univalence axiom and its consequences, and discuss advantages for computer formalization. |
| February 21, 2023 | Everyone | Post colloqium Q & A session |
| March 7, 2023 | Chris Liu | Topos Tuesday - The Subobject Classifier and Logic in Topos Resources: An Invitation to Applied Category Theory - Ch 7 An informal introduction to topos theory |
| April 25, 2023 | Kaylee Fantin‑Hardesty Sarah Lutz |
Title: What Does it Mean for a Word to Have Meaning? Exploring Semantics in Natural Language Processing Abstract: We will start by introducing several elementary solutions for attaching meaning to words in natural language processing, discuss the issues with those, and explore how we can “do better”, i.e. how we can give words more meaning and be more computationally efficient. We end with an overview of Word2vec, a model that uses neural networks to learn word associations, which provides reasonably useful meanings for words. |
Fall 2022
| Date | Speaker | Abstract |
|---|---|---|
| November 17, 2022 | James Wilson | Using the Kleisli & Eillenberg-Moore Theorems |
| November 10, 2022 | Sean Willmot | Monads and adjoint functors |
| November 3, 2022 | Chris Liu | The DisCoCat, Part 2, and Monoidal Categories |
| October 27, 2022 | Ian Jorqueraa | The DisCoCat (Distributional Compositional Categorical) model of meaning |
| September 29, 2022 | Tatum Rask | Categories and Posets |
| September 22, 2022 | Ian Jorqueraa | Examples of functors and natural transformations |
| September 15, 2022 | Alex Elchesen | Functors and Natural Transformations |
| September 8, 2022 | Jacob Cleveland | Categories and Functors, definitions and examples |
Spring 2022
| Date | Speaker | Abstract |
|---|---|---|
| April, 2022 | James Wilson | Towards Higher Inductive Types Youtube |
| March, 2022 | Chris Liu Tatum Rask |
Computable Simplicial Sets, Kan Extensions Youtube |
| February, 2022 | Luke Askew | Simplical Sets |
| February, 2022 | Amit Patel | Linking higher morphisms to topological language Youtube |
| February, 2022 | James Wilson | Computational Equality is Turtles all the way down Youtube |
| January 31, 2022 | Amit Patel | Homotopy and Groupouds Youtube |
Fall 2021
The theme was “logic in categories”.
Topics covered:
- Functional Programming 101 (co-)monads
- Geometric Logic/Axioms of Choice
- Syntax/Semantics
- Quantified Intuitionistic Logic
- Dependent Type Theory
- Martin-Lof Type Theory
- Identity types
- Curry-Howard Isomorphism: a sufficiently verbose proof is indistinguishable from an algorithm.
| Date | Speaker | Abstract |
|---|---|---|
| December 8, 2021 | James Wilson | Subtypes and Mere Propositions Youtube |
| December 1, 2021 | James Wilson | Identity and Inductive Types Youtube |
| November 17, 2021 | Mehdi Rubaii | Martin-Lof Identity Types Youtube |
| November 10, 2021 | Chris Liu Sean Wilmot |
Programming dependent Types, and Proposition as Types Youtube |
| November 3, 2021 | Dustin Tucker | Propositions as Types (Martin-Löf) Youtube |
| October 27, 2021 | Dustin Tucker | Propositions & Judgments (Martin-Löf) Youtube |
| October 13, 2021 | James Wilson | Type Theory - Lambda Calculus |
| October 6, 2021 | James Wilson | Topoi and Tofu |
| September 29, 2021 | Luke Askew | Sheaves in Geometry and Logic |
Fall 2020/Spring 2021
Below were the topics covered. Fill in talks, dates, and abstracts.
- Programs $\iff$ Implicational Intuitionisitic Logic
- Implicational Intuitionistic Logic $\iff$ Simple Type Theories
- Classical Logic $\iff$ Boolean Algebra
- Implicational Intuitionistic Logic $\iff$ Heyting Algebra
- Monads, Adjoints, Abelian Categories, (co-)Limits, Exponentials
- Simple Type Theories $\iff$ Cartesian Closed Categories
- Subobject classifier
- Topos
- Preview Modal/Temporal Logic
- Preview Higher Categories
- Preview Sheafs