Home

Home

Hi!

profile picture I'm Amélia, a non-binary (they/them) mathematician & programmer. This blog is where I write about programming languages: their implementation, their semantics, etc.

cube In addition to this blog, I am the primary maintainer of the 1Lab, an explorable reference resource for mathematics formalised in cubical type theory.

Posts

Here are the lastest 5 posts from the blog:

  • Efficient instance resolution for Agda March 8, 2024

    Translating mathematics into code that a proof assistant can understand is a process that involves a fair bit of friction. There’s quite a big difference between what humans are willing to suspend disbelief about, and what a type checker will actually accept without proof. Reducing this friction is the primary task of the authors of a proof assistant — but, of course, it would be infeasible to modify the proof assistant itself to cover a new problem domain every time one comes up. To this end, we provide users with various mechanisms for automation, through which users can encode their domain-specific knowledge.

  • A quickie: Boundaries in Cubical Agda August 29, 2022

    Wonderfully vague title, yes? As some of you might know, I’m now maintaining the implementation of Cubical Agda. Undoubtedly, if you know, it’s because I’ve been talking your ear off about it: I’m sorry. The “little kid with new toy” energy will continue until morale improves.

  • The Adjoint Functor Theorem in Everyday Life March 13, 2022

    Here’s a mathematical situation that comes up a lot more often than is reasonable. Suppose we have some mathematical object GG, generally defined as some structure on a set: a group, a ring, a topological space. These all have natural categorical structures, so we can - in a uniform way - talk about their subobjects:

  • The Complete History of isoToEquiv December 17, 2021

    It’s a standard fact in (higher) category theory and homotopy theory that any equivalence of categories (homotopy equivalence) can be improved to an adjoint equivalence of categories (strong homotopy equivalence). Adjoint equivalences (and strong homotopy equivalences) are “more structured” notions in the sense that the data of an adjoint equivalence is contractible if inhabited.

  • Parsing Layout, or: Haskell's Syntax is a Mess September 3, 2021

    Hello! Today we’re going to talk about something I’m actually good at, for a change: writing compilers. Specifically, I’m going to demonstrate how to wrangle Alex and Happy to implement a parser for a simple language with the same indentation sensitive parsing behaviour as Haskell, the layout rule.

…or you can find more in the archives.