These are slides and recordings from some talks I've done over the years at various meetup groups and conferences.
- Executable, Synthesizable, Human Readable: Pick Three (intro video): A short walkthrough of a Clash implementation of Pong, as an illustration of the hardware design approach I explore in detail in my upcoming book. (Haskell Love 2021, September 2021)
- ScottCheck: An Adventure in Symbolic Execution (video recording): A whirlwind tour through classic text adventure games, interpreters, SMT solvers, and monad transformer stacks, to answer the eternal question of mankind: "Can you get the coin into the throne room, if it is behind a locked door, and the key is guarded by a vampire?". (Berlin Functional Programming Meetup Group, October 2020)
- Free monoids take a price HIT: a short étude in representing free algebraic structures as syntax modulo theory, using higher inductive types (well, just quotient types, really, but when all you have is a hammer...). Source code of Literate Agda slides contains the Cubical Agda proof that all free monoids are isomorphic. (Haskell.SG meetup, January 2020)
- Cooking a Haskell Curry with Applicative Functors: I was asked to give a talk at the Singapore Institute of Technology for CS students learning FP. I haven't googled these terms, but I'm pretty sure "CS" means "cooking school" and "FP" means "food preparation". This is all based on this old blog post of course, but is updated to use a representation more direct than the (not really correct) free applicative over a co-Yoneda functor. (Singapore Institute of Technology FP Day, March 2019)
- Cubical Type Theory: From i0 to i1, or as I put it on Twitter: Breaking News! Industry programmer writes integer addition in cubical type theory in one week! (Haskell.SG meetup, December 2018)
- Generic Description of Well-Scoped, Well-Typed Syntaxes (Midlands Graduate School, April 2018)
- Resurrecting an 8-bit text adventure game with 5 programming languages and a bit of puzzle solving (Hack && Tell Singapore, July 2017)
- Matt Brown, Jens Palsberg: Typed Self-Evaluation via Intensional Type Functions (Papers We Love.SG ⨯ Haskell.SG, February 2017)
- Pattern Synonyms (Haskell Symposium 2016)
- Compositional Type Checking (video recording) (Haskell.SG meetup, July 2016)
- Matt Brown, Jens Palsberg: Breaking Through the Normalization Barrier: A Self-Interpreter for Fω (Papers We Love.SG, November 2015)
- Conor McBride: "The Derivative of a Regular Type is its Type of One-Hole Contexts" (Paper We Love.SG, June 2015)
- Hobbist FPGA development with Kansas Lava (Haskell.SG meetup, May 2015)
- Practical introduction to Agda (Singapore Functional Meetup, June/July 2012)
- Compositional Type Checking for Hindley-Milner Type Systems with Ad-hoc Polymorphism (Masters thesis defense, January 2011)