Pratap Singh

CS PhD student at CMU

Education

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

Publications

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 and side-channel resistance
  • 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

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

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

Languages: Verus, Dafny, Rust, Haskell, SMT, OCaml, Haskell, Coq, Lean, C/C++, WebAssembly, Python