Pedro Amorim

https://pedrohaa.github.io/

Last Notes

2026-06-18 14:37:37 UTC

- reply

I have thought about this as well. My tongue in cheek way to phrasing it is that the main theorem of your paper should never be "this cursed gadget of mine is a (monoidal, bi, etc) category"

2026-05-23 13:12:57 UTC

- reply

I do a much less organized version of this: I always carry a notebook with me where I work through some calculations, write my thoughts and sketch some ideas.
Its contents are definitely not in pristine condition, since I usually write in it while I'm still thinking about stuff instead of after the fact. When I'm done with a notebook I write on its cover its beginning and end dates, making it much easier to revisit old notes.

2025-10-16 03:03:25 UTC

I'm looking to hire a PhD student to join my group at the University of Bath to work on topics such as categorical logic, programming language theory or categorical probability theory. Here's a description of the position https://pedrohaa.github.io/phd@Bath.pdf . The student is not expected to be well-versed in any of these topics by the time they start their PhD, but should have enough mathematical maturity to be able to learn them throughout their PhD.
The department of Computer Science at the University of Bath has a very active, and expanding, theory group — four new lecturers have been hired over the last year. The position is fully funded for the entire duration of the program (3.5 years) and open to international as well as home students, meaning both tuition fees and a living stipend are covered. The student is expected to start the program in September 2026.
The application deadline is 15/Dec/2025. If this position interests you, please reach out to me.
Reposts are appreciated :)

2025-04-27 17:33:34 UTC

- reply

in Agda they do not coincide because Agda is a terminating language, so you don't get the "limit-colimit coincidence". But in OCaml they actually do coincide!
https://courses.cs.cornell.edu/cs3110/2021sp/textbook/adv/infinite.html
The main issue with OCaml is that its syntax for actually manipulating these infinite structures/solving coinductive fixed point equations is not very good

2025-04-27 09:10:10 UTC

- reply

this is actually a domain theoretic phenomenon, not a laziness one! As a rule of thumb, what distinguishes the calculation of a final coalgebra from that of an initial algebra is that the former is computed as a limit while the latter is computed as a colimit.
However, in many categories enriched over domains, such limits/colimits are the same! I've looked for a more gentle introduction to the topic and wasn't able to find it. A more technical presentation can be found ihe original Smyth and Plotkin paper "the category-theoretic solution of recursive domain equations" or the domain theory notes by Abramsky and Jung

2025-03-20 18:59:58 UTC

- reply

I also skimmed this paper. I think that their particular definition of nominal automata is not *exactly* the same structure as DFAs internal to Nom, but they're almost the same, I think

2025-03-20 13:54:39 UTC

- reply

something I've been toying with recently is working out how should automata theory generalize to other ambient toposes. This would allow you to encompass some well behaved kinds of effects like name generation (automata internal to nominal sets, for instance)