todd

todd, 16 days ago to random

I finally got around to fully merging the Agda implementation of my thesis into @MartinEscardo's library TypeTopology.

TypeTopology contains a variety of theorems written in Agda-style univalent mathematics. It was started by Martin in 2010 and now has many collaborators including @de_Jong_Tom, @ayberkt and @jonmsterling. Among other things, it contains the work of over 20 papers, including two Ph.D. theses.

Check out my thesis, in Agda, here: https://www.cs.bham.ac.uk/~mhe/agda-new/TWA.Thesis.index.html It probably helps to read the thesis itself at the same time, which is here: https://arxiv.org/abs/2401.09270

todd, 8 months ago to random

Hello everyone! I have arrived on Mathstodon now.

If you're in the fortunate position of not knowing me, I am a Teaching Fellow and (until my corrections are done) Ph.D. student at the University of Birmingham, in the School of Computer Science's Theory Group. I am interested in constructive mathematics, univalent type theory and Agda.

My first bit of news is that yesterday I successfully defend my thesis (subject to minor corrections), which concerns formally reasoning in Agda about search algorithms on types for exact real numbers. I was supervised by Dan Ghica and @MartinEscardo.