Education

Publications

Refereed Conference Papers

• 2016
  Chapar: Certified Causally Consistent Distributed Key-Value Stores [Git] [PDF], Mohsen Lesani, Christian J. Bell, Adam Chlipala. Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), January 2016.
• 2013
  Certifiably Sound Parallelizing Transformations (Appendix), Christian J. Bell. Certified Programs and Proofs (CPP), December 2013.
• 2010
  Concurrent Separation Logic for Pipelined Parallelization (Appendix), Christian J. Bell, Andrew W. Appel, David Walker. The 17th Annual Static Analysis Symposium (SAS), September 2010.

Refereed Workshop Publications

• 2016
  A Coinduction Proof Rule for Hoare Doubles [PDF], Christian J. Bell, Adam Chlipala. The Second International Workshop on Coq for PL (CoqPL), January 2016.
• 2013
  Sound Loop Parallelization [slides]. Christian J. Bell. Young Researchers Workshop on Concurrency Theory (YR-CONCUR), August 2013.
• 2008
  Comparing Semantic and Syntactic Methods in Mechanized Proof Frameworks [PDF], Christian J. Bell, Robert Dockins, Aquinas Hobor, Andrew W. Appel, David Walker. 2nd International Workshop on Proof-Carrying Code (PCC), June 2008.

Other

• 2014
  A Proof Theory for Loop-Parallelizing Transformations, Christian J. Bell. Ph.D. Thesis, Princeton University, 35 Olden Street, Princeton NJ, 08540, June 2014.
• 2008
  Control of a Humanoid Robot by a Noninvasive Brain-Computer Interface in Humans [PDF], Christian J. Bell, Pradeep Shenoy, Rawichote Chalodhorn, Rajesh P. N. Rao. Journal of Neural Engineering 5 (2), June 2008.

Talks

• 2015
  Phantom Monitors: A Simple Foundation for Modular Proofs of Fine-Grained Concurrent Programs [slides]. PL Reading Group, Princeton University, November 2015.
• 2015
  Phantom Monitors: A Simple Foundation for Modular Proofs of Fine-Grained Concurrent Programs [slides]. New England Programming Languages Seminar (NEPLS), November 2015.
• 2014
  Verification of Fine-Grained Concurrent Programs [slides]. MIT PL Offsite, May 2014.
• 2013
  Proving the Correctness of Parallelizing Optimizations [slides]. DARPA High-Assurance Cyber Military Systems PI Meeting (HACMS), April 2013.

Teaching

Princeton University

University of Washington

Employment

Awards