About Me

I am a second 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

  • 2022: Software Engineering Intern at Google, Sunnyvale
  • 2020: Software Engineering Intern at Facebook, Menlo Park
  • 2019: Applied Research Mathematician and Software Engineer Intern at the National Security Agency
  • 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 attend various anime conventions

I am a gamer. I like rhythm games (Pump it Up, Dance Dance Revolution, and BeatSaber for example), VR games, puzzle games, and platformers

I also like doing exercise that increases coordination and dexterity. I did parkour for three years (before covid killed the club) and I’ve sampled other similar activities