Mark Bickford

According to our database, Mark Bickford authored at least 34 papers between 1982 and 2022.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2022

Formalizing Moessner's theorem and generalizations in Nuprl.

Mark Bickford, Dexter Kozen, Alexandra Silva

J. Log. Algebraic Methods Program., 2022

2021

Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle.

Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli

Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, 2021

2019

Bar Induction is Compatible with Constructive Type Theory.

Vincent Rahli, Mark Bickford, Liron Cohen, Robert L. Constable

J. ACM, 2019

Implementing Euclid's straightedge and compass constructions in type theory.

Ariel Kellison, Mark Bickford, Robert L. Constable

Ann. Math. Artif. Intell., 2019

2018

Validating Brouwer's continuity principle for numbers using named exceptions.

Vincent Rahli, Mark Bickford

Math. Struct. Comput. Sci., 2018

Connectedness of the continuum in intuitionistic mathematics.

Mark Bickford

Math. Log. Q., 2018

Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl.

Mark Bickford

CoRR, 2018

A Verified Theorem Prover Backend Supported by a Monotonic Library.

Vincent Rahli, Liron Cohen, Mark Bickford

Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

Computability Beyond Church-Turing via Choice Sequences.

Mark Bickford, Liron Cohen, Robert L. Constable, Vincent Rahli

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

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

Bar induction: The good, the bad, and the ugly.

Vincent Rahli, Mark Bickford, Robert L. Constable

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

2016

A nominal exploration of intuitionism.

Vincent Rahli, Mark Bickford

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

2015

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

2014

Intuitionistic completeness of first-order logic.

Robert L. Constable, Mark Bickford

Ann. Pure Appl. Log., 2014

Developing Correctly Replicated Databases Using Formal Tools.

Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable

Proceedings of the 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2014

2013

Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types.

Vincent Rahli, Mark Bickford, Abhishek Anand

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

A diversified and correct-by-construction broadcast service.

Vincent Rahli, Nicolas Schiper, Robbert van Renesse, Mark Bickford, Robert L. Constable

Proceedings of the 20th IEEE International Conference on Network Protocols, 2012

ShadowDB: A Replicated Database on a Synthesized Consensus Core.

Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable

Proceedings of the Eighth Workshop on Hot Topics in System Dependability, HotDep 2012, 2012

2011

Knowledge-Based Synthesis of Distributed Systems Using Event Structures

Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride

Log. Methods Comput. Sci., 2011

2010

Automated Proof of Authentication Protocols in a Logic of Events.

Mark Bickford

Proceedings of the 6th International Verification Workshop, 2010

2009

Component Specification Using Event Classes.

Mark Bickford

Proceedings of the Component-Based Software Engineering, 12th International Symposium, 2009

2008

Unguessable Atoms: A Logical Foundation for Security.

Mark Bickford

Proceedings of the Verified Software: Theories, 2008

Nysiad: Practical Protocol Transformation to Tolerate Byzantine Failures.

Chi Ho, Robbert van Renesse, Mark Bickford, Danny Dolev

Proceedings of the 5th USENIX Symposium on Networked Systems Design & Implementation, 2008

2006

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

2001

Proving Hybrid Protocols Correct.

Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu

Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

Protocol Switching: Exploiting Meta-Properties.

Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable

Proceedings of the 21st International Conference on Distributed Computing Systems Workshops (ICDCS 2001 Workshops), 2001

1999

Predicate Transformers for Infinite-State Automata in NuPRL Type Theory.

Mark Bickford, Jason Hickey

Proceedings of the 3rd Irish Workshop on Formal Methods, Galway, Ireland, July 1999, 1999

1996

Formal Specification and Verification of VHDL.

Mark Bickford, Damir Jamsek

Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

1994

Composable specifications for asynchronous systems using UNITY.

Mark Bickford

Proceedings of the International Symposium on Advanced Research in Asynchronous Circuits and Systems, 1994

1992

Verification of a Fault-Tolerant Property of a Multiprocessor System: A Case Study in Theorem Prover-Based Verification.

Mark Bickford, Mandayam K. Srivas

Proceedings of the Theorem Provers in Circuit Design, 1992

1990

Formal Verification of a Pipelined Microprocessor.

Mandayam K. Srivas, Mark Bickford

IEEE Softw., 1990

A Computer-Aided Verification Tool for Finite State Controller Systems.

Mark Bickford, Mandayam K. Srivas

Proceedings of the Computer-Aided Verification, 1990

1989

Verification of a Pipelined Microprocessor Using Clio.

Mark Bickford, Mandayam K. Srivas

Proceedings of the Hardware Specification, 1989

1982

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