Carnegie Mellon University, Aug 2022-present
PhD student in Computer Science.
Awards: NSF Graduate Research Fellowship, 2023

Harvard University, Sep 2017-Dec 2021
A.B. summa cum laude in Computer Science. Secondary Field in Mathematical Sciences. GPA: 3.99
Relevant coursework: Compilers; Programming Languages; Advanced Topics in Programming Languages; Formal Reasoning about Programs; Operating Systems; Systems Programming and Machine Organization; Data Structures and Algorithms; Theory of Error-correcting Codes; Theoretical Computer Science; Intro. to Probability; Discrete Mathematics
Awards: Phi Beta Kappa (Senior 48), John Harvard Scholar for 2019-2021, Harvard College Scholar for 2018-2019

The Perse School, Cambridge, UK, Class of 2017
A-levels/Pre-U: Mathematics, Further Mathematics, Physics, Chemistry, Economics
Awards: Arkwright Engineering Scholarship, Sixth Form Academic and Music Scholarships


Conference papers

Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh, Andy Wright, and Adam Chlipala, “Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)”. ICFP 2023. View paper

Joshua Gancher, Sydney Gibson, Pratap Singh, Samvid Dharanikota, and Bryan Parno, “Owl: Compositional Verification of Security Protocols via an Information-Flow Type System”. IEEE S&P 2023. View paper

Journal papers

M Sacchi, P Singh, DM Chisnall, DJ Ward, AP Jardine, W Allison, J Ellis, and H Hedgeland, “The dynamics of benzene on Cu(111): a combined helium spin echo and dispersion-corrected DFT study into the diffusion of physisorbed aromatics on metal surfaces”, Faraday Discuss., 2017, 204, 471-485. View paper

H Hedgeland, M Sacchi, P Singh, AJ McIntosh, AP Jardine, G Alexandrowicz, DJ Ward, SJ Jenkins, W Allison, and J Ellis, “Mass Transport in Surface Diffusion of van der Waals Bonded Systems: Boosted by Rotations?”, J. Phys. Chem. Lett., 2016, 7 (23) 4819–4824. View paper

P Singh and H Hedgeland, “Special relativity in the school laboratory: a simple apparatus for cosmic-ray muon detection”, Physics Education, 2015, 50, 317-323. Selected for Physics Education Highlights of 2015. View paper

Projects & Experience

PhD Research on Verified Security Protocol Implementations, Aug 2022–present
School of Computer Science, Carnegie Mellon University, Pittsburgh, PA

  • Developing a proof-producing compiler for security protocols in the Owl language, generating safe, high-performance Rust implementations verified for functional correctness
  • Project repository on GitHub

Research Assistant at MIT PLV, Jan-Aug 2022
Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, MA

  • Implemented support for runtime metrics in the Bedrock2 verified compiler
  • Worked on a model-checker for the RISC-V weak memory model

Research Project on Adapting Verified Compilation for Target-Language Errors, Nov 2020-Dec 2021
School of Engineering and Applied Sciences, Harvard University, Cambridge, MA

  • Studied adaptations to verified compilers that account for target-language errors not present in the source
  • Developed systematization of design space of errors and adaptations

Undergraduate Teaching Fellow, Sept 2018–May 2020, Jan-Dec 2021
Harvard University, Cambridge, MA

  • Courses taught: Computer Science 153 (Compilers) in Fall 2021, Computer Science 152 (Programming Languages) in Spring 2020 and Spring 2021, Computer Science 121 (Introduction to Theoretical Computer Science) in Fall 2019, Applied Mathematics 120 (Applied Linear Algebra and Big Data) in Spring 2019, Mathematics E-23a (Linear Algebra and Real Analysis I) in Fall 2018
  • Taught semester-long Coq section following volume 1 of Pierce’s Software Foundations (Spring 2020, Spring 2021)
  • Held office hours, graded problem sets, and provided one-on-one tutoring and teaching for Harvard College undergraduates and Harvard Extension School distance-learning students
  • Awarded Certificate of Distinction in Teaching for Spring 2019, Spring 2021, Fall 2021 for receiving student evaluation rating above 4.5/5

Investment Associate Intern, June-August 2021
Bridgewater Associates, Westport, CT

  • Conducted group project understanding drivers of equity-market performance
  • Developed inflation forecasts for a specific economy over 2021-2030

Research Project on Verified and Secure Compilation, Feb-Nov 2020
School of Engineering and Applied Sciences, Harvard University, Cambridge, MA

  • Contributed to the Coq development of a verified compiler from IMP to WebAssembly
  • Designed the semantics of the source language and proved type soundness
  • Implemented memory models for the source and target language

Investment Associate Intern, July-August 2020
Bridgewater Associates, Westport, CT

  • Studied macroeconomic theory, asset class fundamentals, and portfolio theory
  • Conducted independent project assessing the macroeconomic outlook of a particular economy during and after the Covid-19 pandemic

Research Project on Dynamic Reflection, Jan-Jul 2020
School of Engineering and Applied Sciences, Harvard University, Cambridge, MA

  • Designed and prototyped several verified reflective systems in Coq including memory instrumentation and a small JIT compiler, and proved soundness of reflection

Summer Project on Sublinear Algorithms in OCaml, June-August 2019
Department of Computer Science and Engineering, IIT Madras, Chennai, India

  • Implemented and evaluated sublinear algorithms including the Count-Min sketch in OCaml for the open-source Owl scientific computing library
  • See related blog post

Harvard College PRISE Fellowship, June–August 2018
Department of Earth and Planetary Sciences, Harvard University, Cambridge, MA

  • Conducted a research project on the suppression of extreme cold events in northern latitude continental interiors under a warmer climate
  • Used Python to run three-dimensional climate simulations and conduct back-trajectory analysis under various warming conditions

Computer Science 50: Final Project, Nov–Dec 2017
Harvard University, Cambridge, MA

  • Designed and implemented a multi-language, multi-user, web-based chat application that automatically translates messages into the appropriate language for each user
  • Tools used: Javascript, Node.js, Python, Flask, Google Translate API

International Summer Science School in Heidelberg, July-August 2016 Center for Quantum Dynamics, University of Heidelberg, Heidelberg, Germany

  • Constructed and characterized optical systems for ultra-cold atom trapping
  • Analyzed optical data using MATLAB and Python

Surface Science Project Research Assistant, June–August 2015
London Centre for Nanotechnology, London, UK

  • Analyzed data sets from helium-3 spin-echo spectrometer using MATLAB, to characterize the diffusive motion of benzene molecules on copper surfaces
  • Ran and analyzed molecular dynamics simulations of benzene molecules on copper surfaces to validate density functional theory models

International Summer School for Young Physicists, July 2015
Perimeter Institute for Theoretical Physics, Waterloo, Ontario, Canada

  • Attended seminars and lectures on aspects of modern physics
  • Carried out a mentor-led project on quantum information theory and computation

Research Project on Relativity in Cosmic-Ray Muons, Sept 2013–March 2015
The Perse School, Cambridge, UK

  • Conducted year-long research project to demonstrate relativistic time dilation by observing the mean lifetimes of cosmic-ray muons
  • Designed and built cosmic-ray telescope using Geiger-Müller tubes and a Raspberry Pi
  • Presented project at UK National Science + Engineering Competition 2015 – awarded Institute of Physics prize

Professional activities

POPL 2023, Boston, MA, USA—Student Volunteer

Oregon Programming Languages Summer School 2022, Eugene, OR, USA—Attended on an OPLSS Scholarship.

POPL 2022, Philadelphia, PA, USA—Student Volunteer

ICFP 2019, Berlin, Germany—Student Volunteer

Technical Skills

Coq, OCaml, Haskell, C/C++, WebAssembly, Python, R, MATLAB, Prolog, LaTeX, Java, Docker


  • Radio – DJ on WHRB, Director of the Jazz Spectrum and Web Manager in 2020
  • Flying – hold a European EASA Private Pilots License, currently have 103 flying hours
  • Clarinet – ABRSM Grade 8 with Distinction, former member of Harvard Band and Wind Ensemble
  • Piano – ABRSM Grade 7