Concurrent Separation Logic for Pipelined Parallelization. - Christian J. Bell; Andrew W. Appel; David Walker 001 (SAS, 2010)

Certifiably Sound Parallelizing Transformations. - Christian J. Bell (CPP, 2013)

A Proof Theory for Loop-Parallelizing Transformations - Christian J. Bell (2014)

Chapar: certified causally consistent distributed key-value stores. - Mohsen Lesani; Christian J. Bell; Adam Chlipala (POPL, 2016)

C4: verified transactional objects. - Mohsen Lesani; Li-yao Xia; Anders Kaseorg; Christian J. Bell; Adam Chlipala; Benjamin C. Pierce; Steve Zdancewic (Proc. ACM Program. Lang., 2022)