I was a postdoc at the University of Manchester working on a variety of things. I’m part of the Autonomy and Verification group.
I spent my PhD encoding the theory of institutions in the Rocq Prover. Formerly known as the Coq proof assistant. You can read about the name change on their website. (It’s all on GitHub.) There are six or so concrete logics encoded there as of this writing, depending on how you count it.
I wrote lots of teaching resources while I was a PhD student at Maynooth. You can see a small selection of them here.
2024
Reasoning about logical systems in the Coq proof assistant.
Reynolds, C., and Monahan, R. Science of Computer Programming, 233, 103054.
Reynolds, C., and Monahan, R. Science of Computer Programming, 233, 103054.
@article{reynolds_reasoning_2024,
title = {Reasoning about logical systems in the {Coq} proof assistant},
volume = {233},
issn = {0167-6423},
url = {https://www.sciencedirect.com/science/article/pii/S0167642323001363},
doi = {10/gs7f2x},
abstract = {The theory of institutions provides an abstract mathematical framework for specifying logical systems and their semantic relationships. Institutions are based on category theory and have deep roots in a well-developed branch of algebraic specification. However, there are no machine-assisted proofs of correctness for institution-theoretic constructions—chiefly satisfaction conditions for institutions and their (co)morphisms—making them difficult to incorporate into mainstream formal methods. This paper therefore provides the details of our approach to formalizing a fragment of the theory of institutions in the Coq proof assistant. We instantiate this framework with the institutions FOPEQ for first-order predicate logic and EVT for the Event-B specification language, and define some institution-independent constructions, all of which serve as an illustration and evaluation of the overall approach.},
urldate = {2023-11-30},
journal = {Science of Computer Programming},
author = {Reynolds, Conor and Monahan, Rosemary},
month = mar,
year = {2024},
pages = {103054},
}2022
Machine-Assisted Proofs for Institutions in Coq.
Reynolds, C., and Monahan, R. In Theoretical Aspects of Software Engineering, (Cham), Springer International Publishing, 180–196.
Reynolds, C., and Monahan, R. In Theoretical Aspects of Software Engineering, (Cham), Springer International Publishing, 180–196.
@inproceedings{reynolds_machine-assisted_2022,
address = {Cham},
title = {Machine-{Assisted} {Proofs} for {Institutions} in {Coq}},
copyright = {All rights reserved},
isbn = {978-3-031-10363-6},
doi = {10/gqfnb6},
booktitle = {Theoretical {Aspects} of {Software} {Engineering}},
publisher = {Springer International Publishing},
author = {Reynolds, Conor and Monahan, Rosemary},
editor = {Aït-Ameur, Yamine and Crăciun, Florin},
year = {2022},
pages = {180–196},
}2021
Using Dafny to Solve the VerifyThis 2021 Challenges.
Farrell, M., Reynolds, C., and Monahan, R. In Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs, (New York, NY, USA), Association for Computing Machinery, 32–38.
Farrell, M., Reynolds, C., and Monahan, R. In Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs, (New York, NY, USA), Association for Computing Machinery, 32–38.
@inproceedings{farrell_using_2021,
address = {New York, NY, USA},
series = {{FTfJP} 2021},
title = {Using {Dafny} to {Solve} the {VerifyThis} 2021 {Challenges}},
isbn = {978-1-4503-8543-5},
doi = {10/gp5v6h},
urldate = {2022-05-16},
booktitle = {Proceedings of the 23rd {ACM} {International} {Workshop} on {Formal} {Techniques} for {Java}-like {Programs}},
publisher = {Association for Computing Machinery},
author = {Farrell, Marie and Reynolds, Conor and Monahan, Rosemary},
month = jul,
year = {2021},
pages = {32–38},
}Formalizing the Institution for Event-B in the Coq Proof Assistant.
Reynolds, C. In Rigorous State-Based Methods, (Cham), Springer International Publishing, 162–166.
Reynolds, C. In Rigorous State-Based Methods, (Cham), Springer International Publishing, 162–166.
@inproceedings{reynolds_formalizing_2021,
address = {Cham},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Formalizing the {Institution} for {Event}-{B} in the {Coq} {Proof} {Assistant}},
copyright = {All rights reserved},
isbn = {978-3-030-77543-8},
doi = {10/gpjt7c},
language = {en},
booktitle = {Rigorous {State}-{Based} {Methods}},
publisher = {Springer International Publishing},
author = {Reynolds, Conor},
editor = {Raschke, Alexander and Méry, Dominique},
year = {2021},
pages = {162–166},
}