Skip to content
View meganfrisella's full-sized avatar
Block or Report

Block or report meganfrisella

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
meganfrisella/README.md

Hi there, I'm Megan!

Pronouns: she/her

I'm a Senior at Brown University studying Math and CS. This GitHub account contains some of the projects I've worked on over the past few years. Please feel free to check them out.

Resarch Interests: Programming languages, software verification, systems

🔬 Research:

  • Improving datacenter efficiency via "soft memory": We propose soft memory: a software level abstraction on top of DRAM that makes memory revocable under memory pressure, for reallocation elsewhere. Our system avoids out-of-memory terminations because soft memory can always be reclaimed from an application to fulfill an immediate request elsewhere. [publication]
  • Proof-oriented imperative programming: I worked on a domain-specific language in F*, called Pulse, for proof-oriented imperative programming. I wrote programs in Pulse to pinpoint proofs that were tricky or awkward to write, and helped design language features and proof syntax that addressed the challenges I discovered. I also implemented an industry-standard measured-boot protocol called DPE in Pulse.
  • Verified cryptographic protocols: I explored the implementation and verification of a key distribution protocol. Using Forge (an Alloy-like model checker), I modeled the protocol and formalized correctness properties for it. Then, I implemented the protocol in Rust and used concepts from Rust ownership and separation logic to do an on-paper proof that the implementation satisfies the correctness properties.

🖥 Teaching:

  • 2-time Head Teaching Assistant for an introductory formal methods course at Brown: CS1710, Logic for Systems.

Email me!

LinkedIn

Note: Sadly, I had issues with my Git email configuration, so my contributions earlier than mid-August, 2021 don't show up accurately 😔

Pinned Loading

  1. shell-types shell-types Public

    Lean

  2. CS1710FinalProject/CS1710FinalProject CS1710FinalProject/CS1710FinalProject Public

    Racket 1

  3. sat-python sat-python Public

    implementing SAT solver in python

    Python 1