Research Activities

My publications are on the home page, if you’re looking for those. Some other things I’m doing or have done:

PhD Thesis

Supervised by Prof Rosemary Monahan, I put institution theory in the Coq proof assistant. You can see it on GitHub.

Institution theory studies logical systems in general using category theory. An institution is a mathematical object which is supposed to approximate a ‘logical system’, and so by studying institutions we hope to study logical systems in general.

I encoded some of the general theory of institutions in Coq and (more significantly) instantiated the theory to a few concrete logics, mostly first-order logic and its variants. I also constructed a trace semantics for Event-B as an institution and combined it with linear temporal logic as a duplex construction.

Work & Education

Awards