About Me

I am a first year PhD at Carnegie Mellon University’s (CMU) Computer Science Department in the areas of programming language theory, type theory, and mechanized verification. My advisor is Karl Crary.

My undergrad was at CMU where I graduated in 2021 with a Computer Science Bachelors

Type Cafe Discord

I’m experimentally running a discord server dedicated to type theory for anyone to join! Please join via this link and introduce yourself!


Conference Papers

  • M. Scharager, K. Cordwell, S. Mitsch, and A. Platzer.
    Verified Quadratic Virtual Subsitution for Real Arithmetic.
    Formal Methods (FM) 2021. (doi | arXiv | AFP)

Preprints/Work in Progress

  • M. Scharager and K. Crary.
    Full Abstraction Correctness of the Continuation Passing Style Translation using Type-Oriented Merging.
    Undergrad Thesis, yet to be published

Teaching Experience

  • 15317 TA: Constructive Logic, Fall 2021
  • 15312 TA: Foundations of Programming Languages, Fall 2020
  • 98038 Co-Instructor: Student Taught Course Anime From Astro Boy to Your Name, Fall 2020 and Spring 2021
  • 15451 TA: Algorithm Design and Analysis, Fall 2019

Work Experience

  • 2020: Software Engineering Intern at Facebook, Menlo Park
  • 2019: Applied Research Mathematician and Software Engineer Intern at the Department of Defense
  • 2018: Cybersecurity Developer Intern at Northrop Grumman Xetron
  • 2015: Machine Shop Intern at Max Planck Florida Institute for Neuroscience


I love watching anime and am involved in anime-like clubs like cosplay

I am a gamer. I like rhythm games (Dance Dance Revolution and BeatSaber for example), VR games, puzzle games, and platformers. Yes, I play league, no, I’m not good at it

I also like doing exercise that increases coordination and dexterity. I have been doing parkour for three years and I’ve sampled other similar activities