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.