Robert Zhang

Scholar, Twitter, GitHub, LinkedIn
jzhan239@jhu.edu
robert-portrait

News
Dec. 22, 2023 · Our paper A Pure Demand Operational Semantics with Applications to Program Analysis has been conditionally accepted to appear at OOPSLA '24!
Aug. 23, 2023 · I'm honored to have been selected as the 2023 Masson Fellow!
May 1, 2023 · I'll be volunteering at PLDI '23 and attending OPLSS!
Feb. 9, 2023 · I led a workshop on JavaScript tooling for JHU ACM.
Jan. 10, 2023 · I'll be at PLMW @ POPL '23!

I'm a final-year Combined B.S./M.S.E. in Computer Science (2019 - 2024) student at Johns Hopkins University. My interests span many topics in programming languages and compilers, including language design, program analysis, formal verification, and type systems.

I'm a member of the JHU Programming Languages Laboratory, working with Professor Scott Smith on novel abstract interpretation models.

In Fall 2024, I'll join UT Austin as a CS PhD student.

Publications
  • A Pure Demand Operational Semantics with Applications to Program Analysis. Scott Smith, Robert Zhang. Conditionally accepted to OOPSLA '24 (preprint, code).
Ongoing Research

  • Pure Demand Operational Semantics

    A novel minimal-state semantics that uses a "stack trace" to look up variables on demand, driving a more precise, compact, and performant static program analysis that does away with the widening step. It executes programs in one go and derives expressive recurrences as results.

    • Fixed/improved theory and implemented various versions of the interpreter and program analysis in OCaml.
    • Extended program analysis to generate CHCs from analysis results and solve them with Z3 for high control flow path sensitivity and verification of final result.
    • Benchmarked analysis performance against Demand-Driven Program Analysis (backwards) and P4F (forwards).
    • Mechanize the interpreter and program analysis in Coq to formally prove determinism, soundness, the former's equivalence to standard interpreters, etc.
    • Co-authored a paper on our work, which has been conditionally accepted to appear at OOPSLA '24.

  • Compiler-Optimized Atomic Execution in Intermittent Computing

    Upon power loss, instructions in an atomic region must restart together. Ocelot automatically analyzes and transforms Rust code for safe and timely intermittent computation. It leverages a hybrid of atomic execution and JIT checkpointing (saving volatile state right before failure) to enforce memory consistency while ensuring freshness and temporal consistency of non-idempotent inputs (e.g., sensor readings).

    • Revamped project to support LLVM 17 and use the new pass manager. Improved C++ code style and added extensive debug logging.
    • Fixed Ocelot's atomic region inference LLVM pass to (1) exhaustively place instructions tainted by the same input into the same region and (2) fully erase instructions associated with fresh/consistent annotations.
    • Extend pass to cluster input-tainted instructions closer together via instruction scheduling, loop unrolling, and function inlining, yielding smaller atomic regions for lower power consumption and greater forward progress.

  • Coq Elaboration for DCS

    DCS is a practical strong functional programming language driven by a sophisticated type-based termination analysis that allows naturally writing divide-and-conquer programs where recursive calls are permitted on values that are not sub-data of the original inputs (e.g., the two halves of a split list in merge sort). DCS uses subtyping to elide the extensive set of coercions required by type checking. Extends essence of POPL '23 paper.

    • Set up continuous integration to build the Haskell project on merge/push for higher code quality assurance.
    • Improved DCS' module system through a more usable import mechanism.
    • Introduce type casts based on subtyping relations to make the implicit coercions explicit.
    • Design and implement in Haskell an elaboration process to compile DCS programs (with explicit coercions) into Coq for further assurance of termination and to prove program properties.
Honors, Awards & Service

  • Masson Fellow 2023 (news article, proposal)

    Established in honor of the Department of Computer Science's inaugural chair, Gerald M. Masson, the fellowship recognizes and supports top students enrolled in the Combined Bachelor's/Master's degree program based on research merit.

  • Member, Upsilon Pi Epsilon

    Upsilon Pi Epsilon is "the first and only, existing international honor society in the Computing and Information disciplines." Selected from a competitive process as one of the 2023 inductees.

  • Dean's Master's Fellow 2023

    Fellowship covering half of the tuition for every semester of full-time, residential enrollment in the master's degree for students who graduate with a Johns Hopkins University undergraduate degree.

  • Student Volunteer, PLDI '23

    Helped with audio/video and real-time streaming; facilitated social events; resolved inquiries from conference attendees at the info desk.

Teaching
Experience
Open Source

  • Author of Lyte: a collection of highly extensible React components.

  • Author of LytePQ: a small and mighty suite of data structures in JavaScript.

  • Creator of trade-ml: a bitcoin trading simulation app implemented in OCaml and ReScript.

  • Co-Founder and CTO of Notest: an AI-enabled question generation note-taking app.

  • Contributor to Modern.js: an open source meta-framework suite.

Older Projects

  • Fractals: A hassle-free all-in-one event planning experience.

  • MyCourses: A light-weight app for searching Johns Hopkins University CS Courses and managing those you took, are taking, and are going to take.

  • BlooChat: A simple yet fluid chatting experience with anyone online.

MIT 2024 © Robert Zhang.