Propositional & analogical generation of coordinated verbal, visual & musical texts: U. of Wisconsin. - Sheldon Klein; David A. Ross; Mark S. Manasse; Johanna Danos; Mark Bickford; Kendall Jensen; Walter A. Burt; Glenn D. Blank; Walter T. Blanks (SIGART Newsl., 1982)

Verification of a Pipelined Microprocessor Using Clio. - Mark Bickford; Mandayam K. Srivas (Hardware Specification, Verification and Synthesis, 1989)

A Computer-Aided Verification Tool for Finite State Controller Systems. - Mark Bickford; Mandayam K. Srivas (CAV (DIMACS/AMS volume), 1990)

Formal Verification of a Pipelined Microprocessor. - Mandayam K. Srivas; Mark Bickford (IEEE Softw., 1990)

Verification of a Fault-Tolerant Property of a Multiprocessor System: A Case Study in Theorem Prover-Based Verification. - Mark Bickford; Mandayam K. Srivas (TPCD, 1992)

Composable specifications for asynchronous systems using UNITY. - Mark Bickford (ASYNC, 1994)

Formal Specification and Verification of VHDL. - Mark Bickford; Damir Jamsek (FMCAD, 1996)

Predicate Transformers for Infinite-State Automata in NuPRL Type Theory. - Mark Bickford; Jason Hickey (IWFM, 1999)

Protocol Switching: Exploiting Meta-Properties. - Xiaoming Liu 003; Robbert van Renesse; Mark Bickford; Christoph Kreitz; Robert L. Constable (ICDCS Workshops, 2001)

Proving Hybrid Protocols Correct. - Mark Bickford; Christoph Kreitz; Robbert van Renesse; Xiaoming Liu 003 (TPHOLs, 2001)

Innovations in computational type theory using Nuprl. - Stuart F. Allen; Mark Bickford; Robert L. Constable; Richard Eaton; Christoph Kreitz; Lori Lorigo; E. Moran (J. Appl. Log., 2006)

Nysiad: Practical Protocol Transformation to Tolerate Byzantine Failures. - Chi Ho; Robbert van Renesse; Mark Bickford; Danny Dolev (NSDI, 2008)

Unguessable Atoms: A Logical Foundation for Security. - Mark Bickford (VSTTE, 2008)

Component Specification Using Event Classes. - Mark Bickford (CBSE, 2009)

Automated Proof of Authentication Protocols in a Logic of Events. - Mark Bickford (VERIFY@IJCAR, 2010)

Knowledge-Based Synthesis of Distributed Systems Using Event Structures - Mark Bickford; Robert L. Constable; Joseph Y. Halpern; Sabina Petride (Log. Methods Comput. Sci., 2011)

ShadowDB: A Replicated Database on a Synthesized Consensus Core. - Nicolas Schiper; Vincent Rahli; Robbert van Renesse; Mark Bickford; Robert L. Constable (HotDep, 2012)

A diversified and correct-by-construction broadcast service. - Vincent Rahli; Nicolas Schiper; Robbert van Renesse; Mark Bickford; Robert L. Constable (ICNP, 2012)

Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types. - Vincent Rahli; Mark Bickford; Abhishek Anand (ITP, 2013)

Developing Correctly Replicated Databases Using Formal Tools. - Nicolas Schiper; Vincent Rahli; Robbert van Renesse; Mark Bickford; Robert L. Constable (DSN, 2014)

Intuitionistic completeness of first-order logic. - Robert L. Constable; Mark Bickford (Ann. Pure Appl. Log., 2014)

Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML. - Vincent Rahli; David Guaspari; Mark Bickford; Robert L. Constable (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2015)

A nominal exploration of intuitionism. - Vincent Rahli; Mark Bickford (CPP, 2016)

Bar induction: The good, the bad, and the ugly. - Vincent Rahli; Mark Bickford; Robert L. Constable (LICS, 2017)

EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems. - Vincent Rahli; David Guaspari; Mark Bickford; Robert L. Constable (Sci. Comput. Program., 2017)

Computability Beyond Church-Turing via Choice Sequences. - Mark Bickford; Liron Cohen 001; Robert L. Constable; Vincent Rahli (LICS, 2018)

A Verified Theorem Prover Backend Supported by a Monotonic Library. - Vincent Rahli; Liron Cohen 001; Mark Bickford (LPAR, 2018)

Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl. - Mark Bickford (CoRR, 2018)

Connectedness of the continuum in intuitionistic mathematics. - Mark Bickford (Math. Log. Q., 2018)

Validating Brouwer's continuity principle for numbers using named exceptions. - Vincent Rahli; Mark Bickford (Math. Struct. Comput. Sci., 2018)

Implementing Euclid's straightedge and compass constructions in type theory. - Ariel Kellison; Mark Bickford; Robert L. Constable (Ann. Math. Artif. Intell., 2019)

Bar Induction is Compatible with Constructive Type Theory. - Vincent Rahli; Mark Bickford; Liron Cohen 001; Robert L. Constable (J. ACM, 2019)

Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle. - Mark Bickford; Liron Cohen 001; Robert L. Constable; Vincent Rahli (CSL, 2021)

Formalizing Moessner's theorem and generalizations in Nuprl. - Mark Bickford; Dexter Kozen; Alexandra Silva 001 (J. Log. Algebraic Methods Program., 2022)