(Old) Research
- Termination Checking for a Functional Programming Language equipped with Higher-Order Data
Supervised by Prof. Brigitte Pientka. Summer 2008.
Funding: NSERC Undergraduate Student Research Award
The goal of the project was to formulate a termination proof (for Beluga) that is based on the notion of structurally recursive terms. For more information, refer to the following papers by Adreas Abel: "Specification and Verification of a Formal System for Structural Recursion", "A Predicative Analysis of Structural Recursion" (Abel, Altenkirch).
- Semantic Considerations on Authorization Logic
Supervised by Prof. Prakash Panangaden. Winter 2008.We played around with the idea of semantic games for an authorization logic. It was fun. It looks like games might be a good way to capture the dependencies established by the says operator used in many authorization logics.
- A Logical Foundation for Authorizing Code Execution
Supervised by Prof. Brigitte Pientka. Funding received for Summer 2007: NSERC Undergraduate Student Research Award, CRA-W Canadian Distributed Mentor Project Award.Abstract. In computer security, resources can be protected by the enforcement of a formally specified access control policy. Policy enforcement implies interaction between a policy specification and program behaviour. We propose to model this interaction with type theory, and present a pure, functional programming language in which access control policies are intrinsic and statically enforced. The underlying type system incorporates constructive authorization logic into contextual modal type theory. As a result, ordinary computation interacts with a policy expressed in authorization logic. Policy enforcement is thus integrated into the software development process, and the secure behaviour of programs is established at compile time.
-
- This project earned me an Honourable Mention in the 2008 Computing Research Association Outstanding Undergraduate Award.
- Poster presented at the McGill University Undergraduate Research Conference on October 19th, 2007.
- Project report to the CRA-W.
- Presentation given at the McGill School of Computer Science Undergraduate Summer Research Symposium.
Feats of undergraduate virtue
Note that the papers posted below most certainly contain errors and silly remarks.
- An Extension of LF: Reasoning about Stateful Deductive Systems with Connectives from Hybrid Logic [pdf]
For COMP-523, Language-Based Security. Based on work by Jason Reed. (2008) - A Case Study of Operational and Denotational Semantics [pdf]
For COMP-627, Theoretical Foundations of Programming Languages (2007)