Knowledge Base of
Publications,
Seminars,
& 
Math Library
PhD theses from the project are accessible at the NCSTRL web site.
Filter for: Mark Bickford
98 results
Cubical type theory with several universes in Nuprl
by Mark Bickford
May 20, 2020
DRAFT: Brouwer's Fixedpoint Theorem in Intuitionistic Mathematics
by Mark Bickford
February 18, 2020
Formalization of Cubical Type Theory in Nuprl
by Mark Bickford
January 15, 2020
Open Bar -- A Reconciliation between Intuitionistic and Classical Logic
by Vincent Rahli, Mark Bickford, Robert L. Constable, Liron Cohen
2020
An Intuitionistic Formalization of The Elements of Euclid Book I
by Ariel Kellison, Mark Bickford
November 26, 2019
Bar Induction is Compatible with Constructive Type Theory
| cite »
by Vincent Rahli, Liron Cohen, Mark Bickford, Robert L. Constable
2019
A Verified Theorem Prover Backend Supported by a Monotonic Library
| cite »
by Vincent Rahli, Liron Cohen, Mark Bickford
November 01, 2018
Validating Brouwer’s Continuity Principle for Numbers Using Named Exceptions
| cite »
by Vincent Rahli, Mark Bickford
January 02, 2018
Computability Beyond Church-Turing using Choice Sequences
| cite »
by Liron Cohen, Vincent Rahli, Mark Bickford, Robert L. Constable
2018
Connectedness of the Continuum in Intuitionistic Mathematics
| cite »
by Mark Bickford
2018
Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl
| cite »
by Mark Bickford
2018
Implementing Euclid's Straightedge and Compass Constructions in Type Theory
| cite »
by Ariel Kellison, Mark Bickford, Robert L. Constable
2018
EventML: Specification, verification, and implementation of crash-tolerant state machine replication systems
| cite »
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
November 15, 2017
Bar Induction: The Good, the Bad, and the Ugly
| cite »
by Vincent Rahli, Mark Bickford, Robert L. Constable
April 11, 2017
Constructive Analysis and Experimental Mathematics using the Nuprl Proof Assistant
by Mark Bickford
March 02, 2016
A Nominal Exploration of Intuitionism
by Vincent Rahli, Mark Bickford
January 18, 2016
Coq as a Metatheory for Nuprl with Bar Induction
by Vincent Rahli, Mark Bickford
September 14, 2015
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
September 01, 2015
Nuprl’s Inductive Logical Forms
by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli
September 01, 2015
Synthetic Topology in NuPRL
by Francisco Mota, Mark Bickford
December 03, 2014
From Replicated Databases to Ensembles of Collaborating Robots
by Abhishek Anand, Mark Bickford
November 19, 2014
Nominal Type Theory
by Mark Bickford, Vincent Rahli
October 29, 2014
Topics in Type Theory
by Abhishek Anand, Robert L. Constable, Mark Bickford
October 22, 2014
There Are No Discontinuous Real Functions
by Mark Bickford, Vincent Rahli
October 08, 2014
Synthesizing Protocols using the Logic of Events and EventML
by Robert L. Constable, Mark Bickford
September 17, 2014
Developing Correctly Replicated Databases Using Formal Tools
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
June 23, 2014
A Fast Algorithm for the Integer Square Root
by Anne Trostle, Mark Bickford
June 09, 2014
A Type Theory with Partial Equivalence Relations as Types
by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli
May 12, 2014
Inductive Construction in Nuprl Type Theory Using Bar Induction
by Mark Bickford, Robert L. Constable
May 12, 2014
Formalizing Bishop's Constructive Analysis in Constructive Type Theory
by Mark Bickford, Robert L. Constable
April 10, 2014
Intuitionistic Completeness of First-Order Logic
| cite »
by Robert L. Constable, Mark Bickford
January 01, 2014
Quotient Types in Nuprl
by Mark Bickford
November 13, 2013
The power of bar induction in constructive type theory
by Mark Bickford
September 25, 2013
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types
| cite »
by Vincent Rahli, Mark Bickford, Abhishek Anand
April 22, 2013
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
March 31, 2013
A Diversified and Correct-by-Construction Broadcast Service
| cite »
by Vincent Rahli, Nicolas Schiper, Robbert van Renesse, Mark Bickford, Robert L. Constable
October 30, 2012
Realizing Bar Induction in Nuprl
by Mark Bickford
October 26, 2012
Bar Induction and the Fan Theorem in Constructive Type Theory
by Robert L. Constable, Mark Bickford, Abhishek Anand
October 12, 2012
ShadowDB: A Replicated Database on a Synthesized Consensus Core
| cite »
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
October 07, 2012
Wider Deployment of Nuprl
by Richard Eaton, Mark Bickford, Robert L. Constable, Christoph Kreitz
September 28, 2012
Formalizing Constructive Analysis in Nuprl
by Mark Bickford
September 04, 2012
Polymorphic Logic
| cite »
by Mark Bickford, Robert L. Constable
July 29, 2012
Formalizing Moessner's Theorem in Nuprl
by Mark Bickford, Dexter Kozen, Alexandra Silva
June 08, 2012
Introduction to EventML
by Mark Bickford, Robert L. Constable, Richard Eaton, David Guaspari
February 03, 2012
The Logic of Events, a framework to reason about distributed systems
| cite »
by Mark Bickford, Vincent Rahli, Robert L. Constable
2012
Adding Communication Primitives to the Nuprl Evaluator
by Mark Bickford
May 04, 2012
Impredicative vs Predicative Type Theory
by Robert L. Constable, Mark Bickford, Richard Eaton
April 13, 2012
Simple Consensus Algorithm
by Robert L. Constable, Mark Bickford, Vincent Rahli
October 28, 2011
NuPRL Demo
by Mark Bickford
September 16, 2011
Intuitionistic Completeness of First-Order Logic
| cite »
by Robert L. Constable, Mark Bickford
October 07, 2011
Automated Proof of Authentication Protocols in a Logic of Events
| cite »
by Mark Bickford
2010
Generating Event Logics with Higher-Order Processes as Realizers
| cite »
by Mark Bickford, Robert L. Constable, David Guaspari
2010
Investigating Correct-by-Construction Attack-Tolerant Systems
| cite »
by Robert L. Constable, Mark Bickford, Robbert van Renesse
2010
Component Specification Using Event Classes
| cite »
by Mark Bickford
2009
Formal Foundations of Computer Security
| cite »
by Mark Bickford, Robert L. Constable
2008
Unguessable Atoms: A Logical Foundation for Security
| cite »
by Mark Bickford
2008
Chain Replication Protocol
by Mark Bickford
September 27, 2006
Formalizing chain replication
by Mark Bickford, David Guaspari
2006
Innovations in Computational Type Theory using Nuprl
| cite »
by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, Evan Moran
2006
Unguessable Atoms: A Logical Foundation for Security
| cite »
by Mark Bickford
2006
Automating Proofs in Event Logic
by Mark Bickford, Richard Eaton
March 23, 2006
Event Systems: Introduction to the Logic of Events
by Mark Bickford
February 17, 2006
Urelements in Type Theory: New Definition of "Inherence"
by Mark Bickford
November 18, 2005
Automated Proofs in Event Logic
by Mark Bickford
September 16, 2005
Automating Proofs in Event Logic
by Mark Bickford, Richard Eaton
August 26, 2005
A Causal Logic of Events in Formalized Computational Type Theory
| cite »
by Mark Bickford, Robert L. Constable
2005
Knowledge-based synthesis of distributed systems using event structures
| cite »
by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2005
A Programming Logic for Distributed Systems
| cite »
by Mark Bickford, David Guaspari
2005
Urelements in Computational Type Theory
by Mark Bickford
November 11, 2005
Real-time Message Automata
by Mark Bickford
February 11, 2005
Mark Presentation
by Mark Bickford
November 29, 2004
Knowledge-Based Synthesis of Distributed Systems Using Event Structures
by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2004
The Logic of Events and Event Structure Patterns
by Mark Bickford
April 26, 2004
Leader Election Protocols
by Mark Bickford
October 06, 2003
Event Systems
by Mark Bickford
November 08, 2003
Graph Theory
by Mark Bickford
May 14, 2003
General Automata Theory
by Mark Bickford
January 25, 2003
A Logic of Events
| cite »
by Mark Bickford, Robert L. Constable
2003
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics
| cite »
by Jon Kleinberg, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz
2003
Implementing the Logic of Events
by Mark Bickford
February 24, 2003
Application of Event Systems and the Logic of Distributed Systems to Leader Election
by Mark Bickford
September 30, 2002
Introduction to Event Systems and the Logic of Distributed Systems
by Mark Bickford, Robert L. Constable
September 16, 2002
Hybrid Protocols
by Mark Bickford
February 20, 2002
FDL: A Prototype Formal Digital Library
by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2002
Recent Results on the PCES Project
by Mark Bickford
April 01, 2002
Report on the DARPA PCES PI meeting
by Robert L. Constable, Lori Lorigo, Mark Bickford
October 29, 2001
Processing video streams using event notification systems
by Robert L. Constable, Mark Bickford
October 15, 2001
More on proof automation: Shostak's decision procedure and Nuprl
by Mark Bickford
September 24, 2001
An Experiment in Formal Design Using Meta-Properties
| cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Robert L. Constable
2001
Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment
| cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse
2001
Protocol Switching: Exploiting Meta-Properties
| cite »
by Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable
2001
Proving Hybrid Protocols Correct
| cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu
2001
Summer Reports
by Stuart F. Allen, Ralph Benzinger, Regina Barzilay, Ozan Hafizogullari, Aleksey Nogin, Amanda Holland-Minkley, Mark Bickford, Sasha Evfimievski, Lori Lorigo
September 18, 2000
Summer Reports
by Stuart F. Allen, Ralph Benzinger, Regina Barzilay, Ozan Hafizogullari, Aleksey Nogin, Amanda Holland-Minkley, Mark Bickford, Sasha Evfimievski, Lori Lorigo
September 11, 2000
Summer Reports
by Stuart F. Allen, Ralph Benzinger, Regina Barzilay, Ozan Hafizogullari, Aleksey Nogin, Amanda Holland-Minkley, Mark Bickford, Sasha Evfimievski, Lori Lorigo
September 04, 2000
Continuation on reflection
by Mark Bickford
March 13, 2000
IO-automata and Ensemble
by Mark Bickford
February 21, 2000
An Object-Oriented Approach to Verifying Group Communication Systems
| cite »
by Mark Bickford, Jason Hickey
1999