Mark Bickford

Publication Activity (10 Years)

Years Active: 1982-2022
Publications (10 Years): 12

Top Topics

Mathematical Knowledge

Quantifier Free

Top Venues

Electron. Commun. Eur. Assoc. Softw. Sci. Technol.

J. Log. Algebraic Methods Program.

Publications

Mark Bickford, Dexter Kozen, Alexandra Silva
Formalizing Moessner's theorem and generalizations in Nuprl. J. Log. Algebraic Methods Program. 124 (2022)
Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli
Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle. CSL (2021)
Vincent Rahli, Mark Bickford, Liron Cohen, Robert L. Constable
Bar Induction is Compatible with Constructive Type Theory. J. ACM 66 (2) (2019)
Ariel Kellison, Mark Bickford, Robert L. Constable
Implementing Euclid's straightedge and compass constructions in type theory. Ann. Math. Artif. Intell. 85 (2-4) (2019)
Mark Bickford
Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl. CoRR (2018)
Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli
Computability Beyond Church-Turing via Choice Sequences. LICS (2018)
Vincent Rahli, Mark Bickford
Validating Brouwer's continuity principle for numbers using named exceptions. Math. Struct. Comput. Sci. 28 (6) (2018)
Mark Bickford
Connectedness of the continuum in intuitionistic mathematics. Math. Log. Q. 64 (4-5) (2018)
Vincent Rahli, Liron Cohen, Mark Bickford
A Verified Theorem Prover Backend Supported by a Monotonic Library. LPAR (2018)
Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems. Sci. Comput. Program. 148 (2017)
Vincent Rahli, Mark Bickford, Robert L. Constable
Bar induction: The good, the bad, and the ugly. LICS (2017)
Vincent Rahli, Mark Bickford
A nominal exploration of intuitionism. CPP (2016)
Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 72 (2015)
Robert L. Constable, Mark Bickford
Intuitionistic completeness of first-order logic. Ann. Pure Appl. Log. 165 (1) (2014)
Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
Developing Correctly Replicated Databases Using Formal Tools. DSN (2014)
Vincent Rahli, Mark Bickford, Abhishek Anand
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types. ITP (2013)
Vincent Rahli, Nicolas Schiper, Robbert van Renesse, Mark Bickford, Robert L. Constable
A diversified and correct-by-construction broadcast service. ICNP (2012)
Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
ShadowDB: A Replicated Database on a Synthesized Consensus Core. HotDep (2012)
Robert L. Constable, Mark Bickford
Intuitionistic Completeness of First-Order Logic CoRR (2011)
Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
Knowledge-Based Synthesis of Distributed Systems Using Event Structures Log. Methods Comput. Sci. 7 (2) (2011)
Mark Bickford
Automated Proof of Authentication Protocols in a Logic of Events. VERIFY@IJCAR (2010)
Mark Bickford
Component Specification Using Event Classes. CBSE (2009)
Mark Bickford
Unguessable Atoms: A Logical Foundation for Security. VSTTE (2008)
Chi Ho, Robbert van Renesse, Mark Bickford, Danny Dolev
Nysiad: Practical Protocol Transformation to Tolerate Byzantine Failures. NSDI (2008)
Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, E. Moran
Innovations in computational type theory using Nuprl. J. Appl. Log. 4 (4) (2006)
Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
Knowledge-Based Synthesis of Distributed Systems Using Event Structures. LPAR (2004)
Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu
Proving Hybrid Protocols Correct. TPHOLs (2001)
Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable
Protocol Switching: Exploiting Meta-Properties. ICDCS Workshops (2001)
Mark Bickford, Jason Hickey
Predicate Transformers for Infinite-State Automata in NuPRL Type Theory. IWFM (1999)
Mark Bickford, Damir Jamsek
Formal Specification and Verification of VHDL. FMCAD (1996)
Mark Bickford
Composable specifications for asynchronous systems using UNITY. ASYNC (1994)
Mark Bickford, Mandayam K. Srivas
Verification of a Fault-Tolerant Property of a Multiprocessor System: A Case Study in Theorem Prover-Based Verification. TPCD (1992)
Mandayam K. Srivas, Mark Bickford
Formal Verification of a Pipelined Microprocessor. IEEE Softw. 7 (5) (1990)
Mark Bickford, Mandayam K. Srivas
A Computer-Aided Verification Tool for Finite State Controller Systems. CAV (DIMACS/AMS volume) (1990)
Mark Bickford, Mandayam K. Srivas
Verification of a Pipelined Microprocessor Using Clio. Hardware Specification, Verification and Synthesis (1989)
Sheldon Klein, David A. Ross, Mark S. Manasse, Johanna Danos, Mark Bickford, Kendall Jensen, Walter A. Burt, Glenn D. Blank, Walter T. Blanks
Propositional & analogical generation of coordinated verbal, visual & musical texts: U. of Wisconsin. SIGART Newsl. 79 (1982)