Posts

POPL Paper—Formalising Graph Algorithms with Coinduction - November 8, 2024
POPL Paper—Algebraic Effects Meet Hoare Logic in Cubical Agda - November 7, 2023
Lazily Grouping in Haskell - October 17, 2022
Depth Comonads - May 3, 2022
Weighted Search Package - August 29, 2021
ICFP Paper—Algebras for Weighted Search - June 21, 2021
Hyperfunctions - March 14, 2021
Master's Thesis - January 4, 2021
Trees indexed by a Cayley Monoid - December 27, 2020
Enumerating Trees - December 14, 2020
A Queue for Effectful Breadth-First Traversals - November 23, 2020
How to set up GitHub Actions for your Agda project - November 18, 2020
Fun with Combinators - October 17, 2020
Some More List Algorithms - August 22, 2020
Presentation on Purely Functional Data Structures - May 19, 2020
More Random Access Lists - May 2, 2020
Another Breadth-First Traversal - February 20, 2020
Typing TABA - February 15, 2020
Terminating Tricky Traversals - January 29, 2020
Lazy Constructive Numbers and the Stern-Brocot Tree - December 14, 2019
A Small Proof that Fin is Injective - November 15, 2019
How to do Binary Random-Access Lists Simply - November 2, 2019
What is Good About Haskell? - October 2, 2019
Bachelor's Thesis - July 14, 2019
Solving Programming Puzzles without using your Brain - June 4, 2019
Deriving a Linear-Time Applicative Traversal of a Rose Tree - May 28, 2019
Implicit Corecursive Queues - May 14, 2019
Concatenative Programming; The Free Monoid of Programming Languages - May 11, 2019
Some Tricks for List Manipulation - May 8, 2019
List Syntax in Agda - April 20, 2019
Probability Monads in Cubical Agda - April 17, 2019
Permutations By Sorting - March 24, 2019
Lazy Binary Numbers - March 21, 2019
More Agda Tips - March 14, 2019
Finger Trees in Agda - February 25, 2019
A New Ring Solver for Agda - January 25, 2019
A Binomial Urn - January 15, 2019
Drawing Trees - December 30, 2018
liftAN - December 29, 2018
Balancing Scans - December 21, 2018
Pure and Lazy Breadth-First Traversals of Graphs in Haskell - December 18, 2018
Prime Sieves in Agda - December 14, 2018
Keeping Formal Verification in Bounds - November 20, 2018
A Very Simple Prime Sieve in Haskell - November 10, 2018
Total Combinations - October 16, 2018
Agda Beginner(-ish) Tips, Tricks, and Pitfalls - September 20, 2018
Verified AVL Trees in Haskell and Agda - July 30, 2018
Probabilistic Functional Programming - July 17, 2018
Probability 5 Ways - June 30, 2018
Scheduling Effects - June 23, 2018
Rotations - June 3, 2018
Breadth-First Traversals in Far Too Much Detail - June 3, 2018
Breadth-First Rose Trees: Traversals and the Cofree Comonad - June 1, 2018
Swapping - May 30, 2018
Sorting Small Things in Haskell - May 6, 2018
Type-Level Induction in Haskell - May 5, 2018
5 Cool Things You Can Do With Pattern Synonyms - April 12, 2018
Strict Applicative Transformer - March 21, 2018
Countdown - March 20, 2018
Convolutions - March 19, 2018
Rose Trees, Breadth-First - March 17, 2018
Choose a random item from a list in one pass - March 15, 2018
Single-Pass Huffman Coding - February 17, 2018
Monadic List Functions - February 11, 2018
groupBy - January 7, 2018
Unfoldl - December 14, 2017
Balancing Folds - October 30, 2017
Convolutions and Semirings - October 13, 2017
Applicative Arithmetic - September 25, 2017
Verifying Data Structures in Haskell - April 23, 2017
Unparsing - April 1, 2017
Fun with Recursion Schemes - March 30, 2017
Constrained Applicatives - March 8, 2017
Semirings - November 17, 2016
Probability Trees - September 30, 2016
A Different Probability Monad - September 27, 2016
Revisiting a Trie in Haskell - September 26, 2016
Lenses are Static Selectors - June 16, 2016
Folding Two Things at Once - April 17, 2016
2048 in Python - October 20, 2015
A Trie in Haskell - October 6, 2015
Faking dependent types in Swift - September 6, 2015
Using Protocols to Build a (very) Generic Deque - August 24, 2015
A Trie in Swift - August 11, 2015
Monty Hall - August 3, 2015
Deques, Queues, and Lists in Swift with Indirect - July 29, 2015
A Strategy for Swift Protocols - July 17, 2015