#
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