Mentor Areas
I study programming languages and computer security. I have wide-ranging interests, and some of my most recent work touches on: Coq verification of LLVM program transformations, type-directed program synthesis, linear types, and quantum computing. I have also spent a lot of time thinking about language-based enforcement of information-flow policies, low-level code memory safety, understanding dynamic security policies, and authorization logic. I am also interested in secure concurrent and distributed computing, functional programming languages, type theory, linear and modal logics, theorem proving and mechanized metatheory.
Description:
1. Use OCaml to build a testing infrastructure for LLVM code, or
2. Learn to do do formal mathematics in the Coq interactive theorem prover.
Other projects are available too. Interested students should contact us to discuss possibilities.
Preferred Qualifications
Experience in functional programming and a strong math background. Relevant coursework includes: CIS 120/121, CIS 341, CIS 500 CIS 552, but you do not have to have taken all of them.
Details:
Preferred Student Year
Junior, Senior
Academic Term
Fall
I prefer to have students start during the above term(s).Volunteer
Yes
Yes indicates that faculty are open to volunteers.Paid
Yes
Yes indicates that faculty are open to paying students they engage in their research, regardless of their work-study eligibility.Work Study
Yes
Yes indicates that faculty are open to hiring work-study-eligible students.