| 2021 | CSL | Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle. | Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli |
| 2018 | LICS | Computability Beyond Church-Turing via Choice Sequences. | Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli |
| 2018 | LPAR | A Verified Theorem Prover Backend Supported by a Monotonic Library. | Vincent Rahli, Liron Cohen, Mark Bickford |
| 2017 | LICS | Bar induction: The good, the bad, and the ugly. | Vincent Rahli, Mark Bickford, Robert L. Constable |
| 2016 | CPP | A nominal exploration of intuitionism. | Vincent Rahli, Mark Bickford |
| 2014 | DSN | Developing Correctly Replicated Databases Using Formal Tools. | Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable |
| 2013 | ITP | Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types. | Vincent Rahli, Mark Bickford, Abhishek Anand |
| 2012 | ICNP | A diversified and correct-by-construction broadcast service. | Vincent Rahli, Nicolas Schiper, Robbert van Renesse, Mark Bickford, Robert L. Constable |
| 2010 | CADE | Automated Proof of Authentication Protocols in a Logic of Events. | Mark Bickford |
| 2008 | NSDI | Nysiad: Practical Protocol Transformation to Tolerate Byzantine Failures. | Chi Ho, Robbert van Renesse, Mark Bickford, Danny Dolev |
| 2004 | LPAR | Knowledge-Based Synthesis of Distributed Systems Using Event Structures. | Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride |
| 1996 | FMCAD | Formal Specification and Verification of VHDL. | Mark Bickford, Damir Jamsek |