I am a computer scientist with interests in programming languages, the theory of computation, and formal methods. In my current research, I investigate how functional programming can help us write parallel programs, and the theoretical models that enable reasoning about the performance of parallel programs. I also have a strong interest for formal methods, and the application of logic and type theory to program verification. I currently work in the programming language research group in Oracle Labs East.

Honors

IFIP 2.8 observer, Annapolis, USA. (2012)

"La Recherche" award in computer science (2011)

Academic service

Program Committee member: 4th Coq workshop (2012)

External Review Committee member: POPL 2012

Misc: NSF panelist (2013), Treasurer for ICFP 2013.

Journal referee: ACM Transation On Programming Languages and Systems, Software Practice & Experience, Information Processing Letters, Higher Order and Symbolic Computation

Conference reviewer: DISC 2013, POPL 2013, CAV 2012, PLDI 2011, PPDP 2010, SSV 2010

Education

Ph.D. in Computer Science, University of Paris, Denis Diderot (2009)

M.Sc. in Computer Science, Ecole normale superieure of Paris (2006)

Appointments

Senior member of technical staff, Oracle labs (2011 - present)

Postdoctoral fellow, Harvard University, School of engineering and Applied Sciences (2009 - 2011)

Research assistant, Microsoft Research/INRIA joint center (2009)

Research assistant, INRIA (2006 - 2009)

Publications

Parallel Programming with BIG Operators. Changhee Park, Guy Steele, and Jean-Baptiste Tristan. 18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPOPP'13).

Rocksalt: Better, Faster, Stronger SFI for the x86. Greg Morrisett, Gang Tan, Joseph Tassarotti, Jean-Baptiste Tristan and Edward Gan. In ACM SIGPLAN 2012 Conference on Programming Language Design and Implementation (PLDI'12).

Evaluating Value-Graph Translation Validation for LLVM. By Jean-Baptiste Tristan, Paul Govereau and Xavier Leroy. In ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation (PLDI'11).

A simple, verified validator for software pipelining. By Jean-Baptiste Tristan and Xavier Leroy.
In 37th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL'10).

Formal Verification of Translation Validators . Jean-Baptiste Tristan. Ph.D. dissertation, University of Paris 7.

Verified Validation of Lazy Code Motion. By Jean-Baptiste Tristan and Xavier Leroy.
In ACM SIGPLAN 2009 Conference on Programming Language Design and Implementation (PLDI'09).

Formal verification of translation validators: A case study on instruction scheduling optimizations . By Jean-Baptiste Tristan and Xavier Leroy. In 35th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL'08).

Teaching

Invited lectures: Harvard CS 153: Principles of Programming Language Compilation (2011). MIT 6.892: Interactive Computer Theorem Proving (2011).

Teaching Fellow: Harvard CS51: Introduction to Computer Science II (2011). Harvard CS50: Introduction to Computer Science I (2010).