Chelsea Battell presentation at Ottawa Mathematics Conference (OMC) June 2016

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)

My master's thesis

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.

LFMTP paper and presentation

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.

CMS winter meeting poster presentation

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.