I have an honours BSc in mathematics from McMaster University and a MSc in mathematics from the University of Ottawa. My main areas of interest are proof theory and formal methods for software engineering.
My master's research accomplishments include contributing to a system called Hybrid for proving things about programming languages. I added a new reasoning layer to help with this process. Using a structural induction proof technique over mutually inductive dependent types, I proved some properties of the logic defining this layer. I also defined a generalization of the new logic to prove theorems more concisely. I have a dream to one day find a simple and elegant explanation of my master's research.
Academic things I've done:
(the presentations are best viewed in full screen without continuous scrolling)
The corresponding Coq code can be found in Hsl_Thesis.v
. The file Hybrid.v
must be compiled first. Coq V8.5 is used for this work.
I presented my work at the Logical Frameworks and Metalanguages: Theory and Practice (LFMTP) Workshop affiliated with the Formal Structures for Computation and Deduction (FSCD) conference in Porto, Portugal in June 2016.
Ottawa Mathematics Conference presentation
I presented a (slightly) higher-level explanation of my research area and contributions at the Ottawa Mathematics Conference in Ottawa, Canada in June 2016.
McGill University Computation and Logic Group presentation
I gave a talk at McGill University in Montreal, Canada in February 2016 where I explained the structure of the system that I contributed to, Hybrid, via an analogy to a garden.
I presented a poster outlining my work-in-progress at the Canadian Mathematical Society Winter Meeting in Montreal, Canada in December 2015 and won the CMS Student Committee Award.
This project was completed as part of a compilers course during my undergrad.