About me

Hi, I'm Matt! I'm currently working as a software engineer and researcher at Galois. In 2019 I graduated from Haverford College with a major in Mathematics and minor in Computer Science, and love tackling challenging problems at the intersection of
 the two.

In computer science I'm interested in:

and in mathematics:

Lately I've been learning a lot about tuning theory, the theoretical side of microtonal music (AKA xenharmonic music). I just added a page to the Xenharmonic wiki discussing how one could modify the Functional Just System to better represent certain types of intervals. To go along with that, I made an interactive webpage for experimenting with different modifications of the FJS. I also made a tool called xen-calc, which streamlines the many different calculations and conversions I found myself doing while learning about the subject.

I love the programming language Agda, and in particular, its cubical mode. In 2019 and 2020 I spent some time contributing to the agda/cubical library – my first major contribution involved representing the integers as a higher inductive type, and perhaps my favorite involved defining the real projective spaces. I've also added homotopy colimits (#175), the dunce cap surface (#214), the pseudo-inverse to truncation (#226), and localization/nullification modalities (#230), the last of which is my most recent and really tested my cubical reasoning.

You can also find here an experiment with formalizing type theory in cubical Agda with Bryn Mawr professor Richard Eisenberg, and here a formalization of some basic knot theory in Agda. I've also contributed to the Glasgow Haskell Compiler, extending Haskell's type system in relation to type families and RULEs.

On the rightBelow is an example of (warning: jargon incoming!) a decomposable lagrangian cobordism between two legendrian knots. The animation is a series of cross-sections of a particular surface which connects two knots: an unknotted loop (the pinched-looking circle) and a trefoil knot. Pictured further below are frames of a decomposable cobordism between the twisted doubles of the same two knots, the construction of which I present in this preprint, coauthored with Haverford professor Josh Sabloff and UPenn postdoctoral fellow Roberta Guadagni.

I also enjoy photography, and dabble in glitch art – for example, the background of this page on desktop. I also love creating theater, and was the lighting designer for 8 student productions over the course of my four years at Haverford.

Send me an email! matthew (at) yacavone (dot) net


Site last updated: June 2021 · Home