Formal verification of translation validators: a case study on instruction scheduling optimizations. - Jean-Baptiste Tristan; Xavier Leroy (POPL, 2008)

Verified validation of lazy code motion. - Jean-Baptiste Tristan; Xavier Leroy (PLDI, 2009)

Formal verification of translation validators. - Jean-Baptiste Tristan (2009)

A simple, verified validator for software pipelining. - Jean-Baptiste Tristan; Xavier Leroy (POPL, 2010)

Evaluating value-graph translation validation for LLVM. - Jean-Baptiste Tristan; Paul Govereau; Greg Morrisett (PLDI, 2011)

RockSalt: better, faster, stronger SFI for the x86. - Greg Morrisett; Gang Tan; Joseph Tassarotti; Jean-Baptiste Tristan; Edward Gan (PLDI, 2012)

Parallel programming with big operators. - Changhee Park; Guy L. Steele Jr.; Jean-Baptiste Tristan (PPoPP, 2013)

Augur: a Modeling Language for Data-Parallel Probabilistic Inference. - Jean-Baptiste Tristan; Daniel Huang 001; Joseph Tassarotti; Adam Craig Pocock; Stephen J. Green; Guy L. Steele Jr. (CoRR, 2013)

Augur: Data-Parallel Probabilistic Modeling. - Jean-Baptiste Tristan; Daniel Huang 001; Joseph Tassarotti; Adam Craig Pocock; Stephen J. Green; Guy L. Steele Jr. (NIPS, 2014)

Efficient Training of LDA on a GPU by Mean-for-Mode Estimation. - Jean-Baptiste Tristan; Joseph Tassarotti; Guy L. Steele Jr. (ICML, 2015)

Using Butterfly-Patterned Partial Sums to Optimize GPU Memory Accesses for Drawing from Discrete Distributions. - Guy L. Steele Jr.; Jean-Baptiste Tristan (CoRR, 2015)

Exponential Stochastic Cellular Automata for Massively Parallel Inference. - Manzil Zaheer; Michael L. Wick; Jean-Baptiste Tristan; Alexander J. Smola; Guy L. Steele Jr. (AISTATS, 2016)

Enforcing Output Constraints via SGD: A Step Towards Neural Lagrangian Relaxation. - Jay Yoon Lee; Michael L. Wick; Jean-Baptiste Tristan; Jaime G. Carbonell (AKBC@NIPS, 2017)

Compiling Markov chain Monte Carlo algorithms for probabilistic modeling. - Daniel Huang 001; Jean-Baptiste Tristan; Greg Morrisett (PLDI, 2017)

Enforcing Constraints on Outputs with Unconstrained Inference. - Jay Yoon Lee; Michael L. Wick; Jean-Baptiste Tristan; Jaime G. Carbonell (CoRR, 2017)

Adding Approximate Counters. - Guy L. Steele Jr.; Jean-Baptiste Tristan (ACM Trans. Parallel Comput., 2017)

Gradient-Based Inference for Networks with Output Constraints. - Jay Yoon Lee; Sanket Vaibhav Mehta; Michael L. Wick; Jean-Baptiste Tristan; Jaime G. Carbonell (AAAI, 2019)

Sketching for Latent Dirichlet-Categorical Models. - Joseph Tassarotti; Jean-Baptiste Tristan; Michael L. Wick (AISTATS, 2019)

Scaling Hierarchical Coreference with Homomorphic Compression. - Michael L. Wick; Swetasudha Panda; Joseph Tassarotti; Jean-Baptiste Tristan (AKBC, 2019)

Unlocking Fairness: a Trade-off Revisited. - Michael L. Wick; Swetasudha Panda; Jean-Baptiste Tristan (NeurIPS, 2019)

A Formal Proof of PAC Learnability for Decision Stumps. - Joseph Tassarotti; Jean-Baptiste Tristan; Koundinya Vajjha (CoRR, 2019)

Using Butterfly-patterned Partial Sums to Draw from Discrete Distributions. - Guy L. Steele Jr.; Jean-Baptiste Tristan (ACM Trans. Parallel Comput., 2019)

Verification of ML Systems via Reparameterization. - Jean-Baptiste Tristan; Joseph Tassarotti; Koundinya Vajjha; Michael L. Wick; Anindya Banerjee 001 (CoRR, 2020)

Detecting and Exorcising Statistical Demons from Language Models with Anti-Models of Negative Data. - Michael L. Wick; Kate Silverstein; Jean-Baptiste Tristan; Adam Craig Pocock; Mark Johnson (CoRR, 2020)

Rate-Regularization and Generalization in Variational Autoencoders. - Alican Bozkurt; Babak Esmaeili 001; Jean-Baptiste Tristan; Dana H. Brooks; Jennifer G. Dy; Jan-Willem van de Meent (AISTATS, 2021)

A formal proof of PAC learnability for decision stumps. - Joseph Tassarotti; Koundinya Vajjha; Anindya Banerjee 001; Jean-Baptiste Tristan (CPP, 2021)

Conjugate Energy-Based Models. - Hao Wu 020; Babak Esmaeili 001; Michael L. Wick; Jean-Baptiste Tristan; Jan-Willem van de Meent (ICML, 2021)

Online Post-Processing in Rankings for Fair Utility Maximization. - Ananya Gupta; Eric Johnson; Justin Payan; Aditya Kumar Roy; Ari Kobren; Swetasudha Panda; Jean-Baptiste Tristan; Michael L. Wick (WSDM, 2021)

On computable learning of continuous features. - Nathanael L. Ackerman; Julian Asilis; Jieqi Di; Cameron E. Freer; Jean-Baptiste Tristan (CoRR, 2021)

Computable PAC Learning of Continuous Features. - Nathanael L. Ackerman; Julian Asilis; Jieqi Di; Cameron E. Freer; Jean-Baptiste Tristan (LICS, 2022)

Verified Density Compilation for a Probabilistic Programming Language. - Joseph Tassarotti; Jean-Baptiste Tristan (Proc. ACM Program. Lang., 2023)

Randomised Testing of the Compiler for a Verification-Aware Programming Language. - Alastair F. Donaldson; Dilan Sheth; Jean-Baptiste Tristan; Alex Usher (ICST, 2024)

Formally Verified Cloud-Scale Authorization. - Aleks Chakarov; Jaco Geldenhuys; Matthew Heck; Michael Hicks 001; Sam Huang; Georges-Axel Jaloyan; Anjali Joshi; K. Rustan M. Leino; Mikael Mayer; Sean McLaughlin; Akhilesh Mritunjai; Clément Pit-Claudel; et al. (ICSE, 2025)

Verified Foundations for Differential Privacy. - Markus de Medeiros; Muhammad Naveed; Tancrède Lepoint; Temesghen Kahsai; Tristan Ravitch; Stefan Zetzsche; Anjali Joshi; Joseph Tassarotti; Aws Albarghouthi; Jean-Baptiste Tristan (Proc. ACM Program. Lang., 2025)

Verifying the Fisher-Yates Shuffle Algorithm in Dafny. - Stefan Zetzsche; Jean-Baptiste Tristan; Tancrède Lepoint; Mikael Mayer (CoRR, 2025)