Email: jt...@andrew.cmu.edu

I am a fourth year Ph.D. student in the Computer Science Department at CMU. My advisor is Robert Harper. I'm interested in programming languages, formal verification, and mathematical logic.

As an undergraduate, I worked with Greg Morrisett as part of the GoNative project. I spent the summer of 2014 as an intern at MPI-SWS, advised by Derek Dreyer and Viktor Vafeiadis. In the summer of 2013, I interned at Oracle Labs working with Guy Steele and Jean-Baptiste Tristan. The summer before that, I was an intern at Inria as a member of the Gallium team under the supervision of Xavier Leroy.

# Papers

# Teaching

# Blog Posts

I am a fourth year Ph.D. student in the Computer Science Department at CMU. My advisor is Robert Harper. I'm interested in programming languages, formal verification, and mathematical logic.

As an undergraduate, I worked with Greg Morrisett as part of the GoNative project. I spent the summer of 2014 as an intern at MPI-SWS, advised by Derek Dreyer and Viktor Vafeiadis. In the summer of 2013, I interned at Oracle Labs working with Guy Steele and Jean-Baptiste Tristan. The summer before that, I was an intern at Inria as a member of the Gallium team under the supervision of Xavier Leroy.

*A Higher-Order Logic for Concurrent Termination-Preserving Refinement*

J. Tassarotti, R. Jung, R. Harper.

**Draft, 2016.**[.pdf] [website with Coq source]*Efficient Training of LDA on a GPU by Mean-for-Mode Estimation.*

J.B. Tristan, J. Tassarotti, G. L. Steele Jr.

**ICML 2015**[.pdf]*Verifying Read-Copy-Update in a Logic for Weak Memory.*

J. Tassarotti, D. Dreyer, V. Vafeiadis.

**PLDI 2015**[.pdf] [website with Coq source]*Augur: Data-Parallel Probabilistic Modeling.*

J.B. Tristan, D. Huang, J. Tassarotti, A. C. Pocock, S. J. Green, G. L. Steele Jr.

**NIPS 2014**[.pdf]*RockSalt: Better, Faster, Stronger SFI for the x86.*

G. Morrisett, G. Tan, J. Tassarotti, J.B. Tristan, and E. Gan.

**PLDI 2012**[.pdf]

- Spring 2015 — TA for 15-312 Foundations of Programming Languages
- Fall 2014 — TA for 15-317 Constructive Logic

- 04 Aug 2012 » Register Allocation in CompCert
- 14 May 2012 » Gas Cans and Decks of Cards
- 30 Dec 2011 » Tarski's High School Algebra Problem