Jamie Fulford

Bio

I’m a second-year Ph.D. student in Computer Science at the University of Illinois Urbana-Champaign, advised by Talia Ringer. I work in programming languages and formal methods, with interests in interactive theorem proving and proof autoformalization. Before Illinois, I studied Computer Science and Mathematics at the University of Virginia (B.S. 2025).

Current Research

• DARPA expMath: building tooling for proof autoformalization and proof decomposition in Agda, targeting homotopy type theory. The tooling breaks a theorem statement into multiple lemmas and sends them to automated provers.
• Proof translation between program logics: designing languages with specific interpretable properties, then implementing them in Rocq so that they interoperate and proofs can be compiled between them.

Previous Research

• Virginia Tech Systems Software Research Group (January – July 2025): proof engineer. Developed type systems and compiler verification for Linux eBPF in Rocq, proving kernel safety properties. Extended the CompCert verified compiler to a new frontend language.
• University of Pennsylvania (Summer 2024): research fellow in the NSF REU in Programming Languages, advised by Steve Zdancewic. Designed and formalized a new lambda calculus for parallel and distributed computation in Rocq, with machine-checked proofs of type safety and confluence.

Formalizations

• Formalizing LLM Guardrails with AgentSpec in Lean 4 (Fall 2025)
• ProbaLean: A Probabilistic DSL in Lean 4 (Spring 2026)

Awards

• PLMW Scholarship, Programming Languages Mentoring Workshop at POPL 2025

Skills

• Proof assistants: Agda, Rocq, Lean 4
• Verification: Iris, CompCert, Mathlib
• Languages: OCaml, Haskell, Rust, Python, C, C++, Java, JavaScript, SQL, Bash
• Tools: Git, Linux, NixOS, LaTeX, PyTorch