Hi, I'm Matt! I’m a software engineer with a background in pure mathematics and computer science research, and a passion for creating digital tools that help explain difficult concepts.

In my spare time while working as a Software Engineer / Researcher at Galois I’ve created interactive webpages for understanding:

- Microtonal music theory, through xen-calc and FJS Explorer
- Judaism, through Visual Tanakh and Interactive Translations
- Linguistics, through a work-in-progress vowel space visualizer

Before Galois I graduated from Haverford College with a major in Mathematics and a minor in Computer Science, and I have always loved tackling challenging problems at the intersection of the two.

The open-source work I've done at Galois has mostly revolved around contributing to SAW and contributing to Cryptol, Galois' open-source tools for formal verification and cryptographic specification, respectively. In particular, I've spent a lot of time working with Eddy Westbrook on the Heapster and Mr. Solver extensions to SAW, which use logics based on separation types and Interaction Trees, respectively, to enable easy and automatic verification of unbounded programs. This work has resulted in two papers, which we wrote along with collaborators at UPenn:

- Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification by Lucas Silver (UPenn), Eddy Westbrook,
*Matthew Yacavone*, and Ryan Scott – published at ECOOP 2023 - A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs by Paul He (UPenn), Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Ştefănescu, Aaron Tomb, Adam Wick,
*Matthew Yacavone*, and Steve Zdancewic – published at OOPSLA 2021

Outside of work, in 2021 I made a brief foray into tuning theory: the theoretical side of microtonal music (AKA xenharmonic music). I created a tool called xen-calc, which streamlines the many different calculations and conversions I found myself doing while learning about the subject. Links to xen-calc have since been added to the sidebar of every interval in the Xenharmonic Wiki (e.g. en.xen.wiki/w/5/4). While working on xen-calc I authored a page on 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.

Around the time I graduated college I fell in 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 general construction, which lifts decomposable cobordisms on legendrian knots to decomposable cobordisms on twisted *n*-copies of the knots, is given by me in Section 4 of the paper:

- Legendrian Satellites and Decomposable Cobordisms by (in alphabetical order) Roberta Guadagni (UPenn), Josh Sabloff (Haverford), and
*Matthew Yacavone*- published in the Journal of Knot Theory and Its Ramifications 2022

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: August 2024 · Home