# Knowledge Base list of Publications

PhD theses from the project are accessible at the NCSTRL web site.

## List by Author

480 results

Aagaard, Mark

*
Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization *
| cite »

by John O'Leary, Miriam Leeser, Jason Hickey, Mark Aagaard

1994

*
Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification *
| cite »

by Mark Aagaard, Miriam Leeser

1993

Aitken, William

*
Metalogical Frameworks II: Developing a Reflected Decision Procedure *
| cite »

by William Aitken, Robert L. Constable, Judith Underwood

1999

*
The Semantics of Reflected Proof *
| cite »

by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken

1990

Allen, Stuart F.

*
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

*
Enabling Large Scale Coherency Among Mathematical Texts *
| cite »

by Stuart F. Allen, Robert L. Constable

2006

*
Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts *
| cite »

by Stuart F. Allen, Robert L. Constable, Lori Lorigo

2006

*
An Abstract Semantics for Atoms in Nuprl *
| cite »

by Stuart F. Allen

2006

*
Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations *
| cite »

by Stuart F. Allen, Robert L. Constable, Matthew Fluet

2004

*
Abstract Identifiers, Intertextual Reference and a Computational Basis for Recordkeeping *
| cite »

by Stuart F. Allen

2004

*
Practical Reflection in Nuprl *
| cite »

by Eli Barzilay, Stuart F. Allen, Robert L. Constable

2003

*
Abstract Identifiers and Textual Reference *
| cite »

by Stuart F. Allen

2002

*
Reflecting Higher-Order Abstract Syntax in Nuprl *
| cite »

by Eli Barzilay, Stuart F. Allen

2002

*
FDL: A Prototype Formal Digital Library *

by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2002

*
Logical Aspects of Digital Mathematics Libraries (extended abstract) *
| cite »

by Stuart F. Allen, James L. Caldwell, Robert L. Constable

2001

*
The Nuprl Open Logical Environment *
| cite »

by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2000

*
From dy/dx to []P: A Matter of Notation *
| cite »

by Stuart F. Allen

1998

*
The Semantics of Reflected Proof *
| cite »

by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken

1990

*
Reflecting the Open-Ended Computation System of Constructive Type Theory *
| cite »

by Robert L. Constable, Stuart F. Allen, Douglas J. Howe

1990

*
A Non-Type-Theoretic Definition of Martin-Lof's Types *
| cite »

by Stuart F. Allen

1987

*
A Non-Type-Theoretic Semantics for Type-Theoretic Language *
| cite »

by Stuart F. Allen

1987

*
Implementing Mathematics with the Nuprl Development System *
| cite »

by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith

1986

Anand, Abhishek

*
A Type Theory with Partial Equivalence Relations as Types *

by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli

May 12, 2014

*
Towards a Formally Verified Proof Assistant *

by Abhishek Anand, Vincent Rahli

July 14, 2014

*
A Generic Approach to Proofs about Substitution *

by Abhishek Anand, Vincent Rahli

July 17, 2014

*
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types *
| cite »

by Vincent Rahli, Mark Bickford, Abhishek Anand

April 22, 2013

Aydemir, Brian

*
MetaPRL -- A Modular Logical Environment *
| cite »

by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo

2003

Barzilay, Eli

*
Implementing Reflection in Nuprl *
| cite »

by Eli Barzilay

2006

*
Practical Reflection in Nuprl *
| cite »

by Eli Barzilay, Stuart F. Allen, Robert L. Constable

2003

*
MetaPRL -- A Modular Logical Environment *
| cite »

by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo

2003

*
Reflecting Higher-Order Abstract Syntax in Nuprl *
| cite »

by Eli Barzilay, Stuart F. Allen

2002

*
Quotation and Reflection in Nuprl and Scheme *
| cite »

by Eli Barzilay

2001

Barzilay, Regina

*
Verbalization of High-Level Formal Proofs *
| cite »

by Amanda Holland-Minkley, Regina Barzilay, Robert L. Constable

1999

Basin, David A.

*
Extracting Circuits from Constructive Proofs *
| cite »

by David A. Basin

1991

*
Formally Verified Synthesis of Combinational Circuits *
| cite »

by David A. Basin, Geoffrey Brown, Miriam Leeser

1991

*
Metalogical Frameworks *
| cite »

by David A. Basin, Robert L. Constable

1991

*
Some Normalization Properties of Martin-Lof's Type Theory and Applications *
| cite »

by David A. Basin, Douglas J. Howe

1991

*
Building Problem Solving Environments in Constructive Type Theory *
| cite »

by David A. Basin

1990

*
Building Theories in Nuprl *
| cite »

by David A. Basin

1989

*
Verification of Combinational Logic in Nuprl *
| cite »

by David A. Basin, Peter Del Vecchio

1989

*
An Environment for Automated Reasoning About Partial Functions *
| cite »

by David A. Basin

1988

Bates, Joseph L.

*
Proofs as Programs *
| cite »

by Joseph L. Bates, Robert L. Constable

1985

*
Writing Programs That Construct Proofs *
| cite »

by Robert L. Constable, Todd B. Knoblock, Joseph L. Bates

1984

*
A Logic for Correct Program Development *
| cite »

by Joseph L. Bates

1981

Benzinger, Ralph

*
Automated Complexity Analysis of Nuprl Extracted Programs *
| cite »

by Ralph Benzinger

2001

*
Automated Computational Complexity Analysis *
| cite »

by Ralph Benzinger

2001

Berger, Ulrich

*
Logic, Construction, Computation *
| cite »

by Ulrich Berger

July 29, 2012

Bickford, Mark

*
Formalization of Cubical Type Theory in Nuprl *

by Mark Bickford

January 15, 2020

*
DRAFT: Brouwer's Fixedpoint Theorem in Intuitionistic Mathematics *

by Mark Bickford

February 18, 2020

*
Open Bar -- A Reconciliation between Intuitionistic and Classical Logic *

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

2020

*
Cubical type theory with several universes in Nuprl *

by Mark Bickford

May 20, 2020

*
Bar Induction is Compatible with Constructive Type Theory *
| cite »

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

2019

*
Validating Brouwer’s Continuity Principle for Numbers Using Named Exceptions *
| cite »

by Vincent Rahli, Mark Bickford

January 02, 2018

*
Connectedness of the Continuum in Intuitionistic Mathematics *
| cite »

by Mark Bickford

2018

*
Computability Beyond Church-Turing using Choice Sequences *
| cite »

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

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

*
A Verified Theorem Prover Backend Supported by a Monotonic Library *
| cite »

by Vincent Rahli, Liron Cohen, Mark Bickford

November 01, 2018

*
Bar Induction: The Good, the Bad, and the Ugly *
| cite »

by Vincent Rahli, Mark Bickford, Robert L. Constable

April 11, 2017

*
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

*
A Nominal Exploration of Intuitionism *

by Vincent Rahli, Mark Bickford

January 18, 2016

*
Constructive Analysis and Experimental Mathematics using the Nuprl Proof Assistant *

by Mark Bickford

March 02, 2016

*
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML *

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

September 01, 2015

*
Coq as a Metatheory for Nuprl with Bar Induction *

by Vincent Rahli, Mark Bickford

September 14, 2015

*
Nuprl’s Inductive Logical Forms *

by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli

September 01, 2015

*
Intuitionistic Completeness of First-Order Logic *
| cite »

by Robert L. Constable, Mark Bickford

January 01, 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 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

*
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

*
The Logic of Events, a framework to reason about distributed systems *
| cite »

by Mark Bickford, Vincent Rahli, Robert L. Constable

2012

*
Polymorphic Logic *
| cite »

by Mark Bickford, Robert L. Constable

July 29, 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

*
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

*
Intuitionistic Completeness of First-Order Logic *
| cite »

by Robert L. Constable, Mark Bickford

October 07, 2011

*
Generating Event Logics with Higher-Order Processes as Realizers *
| cite »

by Mark Bickford, Robert L. Constable, David Guaspari

2010

*
Automated Proof of Authentication Protocols in a Logic of Events *
| cite »

by Mark Bickford

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

*
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

*
Formalizing chain replication *

by Mark Bickford, David Guaspari

2006

*
Unguessable Atoms: A Logical Foundation for Security *
| cite »

by Mark Bickford

2006

*
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

*
Knowledge-Based Synthesis of Distributed Systems Using Event Structures *

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

2004

*
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics *
| cite »

by Jon Kleinberg, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz

2003

*
A Logic of Events *
| cite »

by Mark Bickford, Robert L. Constable

2003

*
FDL: A Prototype Formal Digital Library *

by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2002

*
An Experiment in Formal Design Using Meta-Properties *
| cite »

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

2001

*
Proving Hybrid Protocols Correct *
| cite »

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

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

*
An Object-Oriented Approach to Verifying Group Communication Systems *
| cite »

by Mark Bickford, Jason Hickey

1999

Birman, Kenneth

*
The Horus and Ensemble Projects: Accomplishments and Limitations *
| cite »

by Kenneth Birman, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, Werner Vogels

2000

*
Building Reliable, High-Performance Communication Systems from Components *
| cite »

by Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, Robert L. Constable

1999

Bromley, H. M.

*
Implementing Mathematics with the Nuprl Development System *
| cite »

by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith

1986

Brown, Geoffrey

*
Formally Verified Synthesis of Combinational Circuits *
| cite »

by David A. Basin, Geoffrey Brown, Miriam Leeser

1991

Bundy, Alan

*
The Oyster-Clam System *
| cite »

by Alan Bundy, Frank Van Harmelen, Christian Horn, Alan Smaill

1990

Caldwell, James L.

*
Logical Aspects of Digital Mathematics Libraries (extended abstract) *
| cite »

by Stuart F. Allen, James L. Caldwell, Robert L. Constable

2001

*
Search Algorithms in Type Theory *
| cite »

by James L. Caldwell, Ian Gent, Judith Underwood

2000

*
Intuitionistic Tableau Extracted *
| cite »

by James L. Caldwell

1999

*
Classical Propositional Decidability via Nuprl Proof Extraction *
| cite »

by James L. Caldwell

1998

*
Decidability Extracted: Synthesizing *
| cite »

by James L. Caldwell

1998

*
Extracting Propositional Decidability: A Proof of Propositional Decidability in Constructive Type Theory and its Extracted Program *
| cite »

by James L. Caldwell

1997

*
Moving Proofs-as-Programs into Practice *
| cite »

by James L. Caldwell

1997

*
Classical Tools for Constructive Proof Search *
| cite »

by James L. Caldwell, Judith Underwood

1996

Chan, Tat-hung

*
Reversal-Bounded Computations *
| cite »

by Tat-hung Chan

1980

Chen, Wilfred Z.

*
Tactic-Based Theorem Proving and Knowledge-Based Forward Chaining: An Experiment with Nuprl and Ontic *
| cite »

by Wilfred Z. Chen

1992

Cheung, Crystal

*
Brouwer's Fan Theorem: An Overview *

by Crystal Cheung

2015

Chew, Paul

*
Collaborative Mathematics Environments *
| cite »

by Robert L. Constable, Paul Chew, Keshav Pingali, Steve Vavasis, Richard Zippel

1996

Cleaveland, Walter Rance

*
Type-Theoretic Models of Concurrency *
| cite »

by Walter Rance Cleaveland

1987

*
Implementing Mathematics with the Nuprl Development System *
| cite »

by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith

1986

Cohen, Liron

*
Open Bar -- A Reconciliation between Intuitionistic and Classical Logic *

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

2020

*
Bar Induction is Compatible with Constructive Type Theory *
| cite »

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

2019

*
Automated Reasoning in Herbrand Structures *

by Liron Cohen, Reuben Rowe, Yoni Zohar

June 03, 2019

*
Computability Beyond Church-Turing using Choice Sequences *
| cite »

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

2018

*
A Verified Theorem Prover Backend Supported by a Monotonic Library *
| cite »

by Vincent Rahli, Liron Cohen, Mark Bickford

November 01, 2018

*
Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent *
| cite »

by Liron Cohen, Reuben Rowe

July 01, 2018

*
Intuitionistic Ancestral Logic *

by Liron Cohen, Robert L. Constable

October 10, 2015

Constable, Robert L.

*
Computer Science at the Frontiers of Mathematics *

by Robert L. Constable

January 15, 2020

*
The Continuum *

by Robert L. Constable

February 26, 2020

*
Open Bar -- A Reconciliation between Intuitionistic and Classical Logic *

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

2020

*
Bar Induction is Compatible with Constructive Type Theory *
| cite »

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

2019

*
Computability Beyond Church-Turing using Choice Sequences *
| cite »

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

2018

*
Implementing Euclid's Straightedge and Compass Constructions in Type Theory *
| cite »

by Ariel Kellison, Mark Bickford, Robert L. Constable

2018

*
Bar Induction: The Good, the Bad, and the Ugly *
| cite »

by Vincent Rahli, Mark Bickford, Robert L. Constable

April 11, 2017

*
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

*
A Formal Exploration of Constructive Geometry *

by Robert L. Constable, Sarah Sernaker

2016

*
Intuitionistic Ancestral Logic *

by Liron Cohen, Robert L. Constable

October 10, 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

*
Intuitionistic Completeness of First-Order Logic *
| cite »

by Robert L. Constable, Mark Bickford

January 01, 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 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

*
Virtual Evidence: A Constructive Semantics for Classical Logics *

by Robert L. Constable

2014

*
The Logic of Information Flow and the Foundations of Distributed Computing *

by Robert L. Constable

January 10, 2013

*
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems *

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

March 31, 2013

*
The Logic of Events, a framework to reason about distributed systems *
| cite »

by Mark Bickford, Vincent Rahli, Robert L. Constable

2012

*
Proof Assistants and the Rise of Type Theory Circa 1912-2012 *

by Robert L. Constable

March 19, 2012

*
Type Theoretic Semantics for First-Order Logic *

by Robert L. Constable

May 24, 2012

*
Proof Assistants and the Dynamic Nature of Formal Theories *
| cite »

by Robert L. Constable

June 29, 2012

*
On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer *
| cite »

by Robert L. Constable

June 29, 2012

*
Polymorphic Logic *
| cite »

by Mark Bickford, Robert L. Constable

July 29, 2012

*
Proofs as Process *

by Robert L. Constable

2012

*
Russell's Orders in Kripke's Theory of Truth and Computational Type Theory *
| cite »

by Robert L. Constable, Fairouz Kamareddine, Twan Laan

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

*
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

*
Next Generation Proof Technology *

by Robert L. Constable

December 27, 2012

*
Intuitionistic Completeness of First-Order Logic *
| cite »

by Robert L. Constable, Mark Bickford

October 07, 2011

*
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

*
The Triumph of Types: Principia Mathematica's Impact on Computer Science *
| cite »

by Robert L. Constable

2010

*
Building Mathematics-Based Software Systems to Advance Science and Create Knowledge *
| cite »

by Robert L. Constable

2009

*
Formal Foundations of Computer Security *
| cite »

by Mark Bickford, Robert L. Constable

2008

*
Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP *
| cite »

by Robert L. Constable

2008

*
Computational Type Theory -- Extended Version *
| cite »

by Robert L. Constable

2008

*
Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus *
| cite »

by Wojciech Moczydlowski, Robert L. Constable

2007

*
Transforming the Academy: Knowledge Formation in the Age of Digital Information *

by Robert L. Constable

January 11, 2007

*
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

*
Enabling Large Scale Coherency Among Mathematical Texts *
| cite »

by Stuart F. Allen, Robert L. Constable

2006

*
Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts *
| cite »

by Stuart F. Allen, Robert L. Constable, Lori Lorigo

2006

*
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics *
| cite »

by Robert L. Constable, Wojciech Moczydlowski

2006

*
Information-Intensive Proof Technology *
| cite »

by Robert L. Constable

2006

*
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

*
Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations *
| cite »

by Stuart F. Allen, Robert L. Constable, Matthew Fluet

2004

*
Knowledge-Based Synthesis of Distributed Systems Using Event Structures *

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

2004

*
A Graph-Based Approach towards Discerning Inherent Structures in a Digital Library of Formal Mathematics. *
| cite »

by Lori Lorigo, Jon Kleinberg, Richard Eaton, Robert L. Constable

2004

*
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics *
| cite »

by Jon Kleinberg, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz

2003

*
Practical Reflection in Nuprl *
| cite »

by Eli Barzilay, Stuart F. Allen, Robert L. Constable

2003

*
A Logic of Events *
| cite »

by Mark Bickford, Robert L. Constable

2003

*
Recent Results in Type Theory and Their Relationship to Automath *
| cite »

by Robert L. Constable

2003

*
MetaPRL -- A Modular Logical Environment *
| cite »

by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo

2003

*
Computational Complexity and Induction for Partial Computable Functions in Type Theory *
| cite »

by Robert L. Constable, Karl Crary

2002

*
Naive Computational Type Theory *
| cite »

by Robert L. Constable

2002

*
FDL: A Prototype Formal Digital Library *

by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2002

*
Logical Aspects of Digital Mathematics Libraries (extended abstract) *
| cite »

by Stuart F. Allen, James L. Caldwell, Robert L. Constable

2001

*
An Experiment in Formal Design Using Meta-Properties *
| cite »

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

2001

*
Protocol Switching: Exploiting Meta-Properties *
| cite »

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

2001

*
The Nuprl Open Logical Environment *
| cite »

by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2000

*
The Horus and Ensemble Projects: Accomplishments and Limitations *
| cite »

by Kenneth Birman, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, Werner Vogels

2000

*
Nuprl's Class Theory and Its Applications *
| cite »

by Robert L. Constable, Jason Hickey

2000

*
Verbalization of High-Level Formal Proofs *
| cite »

by Amanda Holland-Minkley, Regina Barzilay, Robert L. Constable

1999

*
Metalogical Frameworks II: Developing a Reflected Decision Procedure *
| cite »

by William Aitken, Robert L. Constable, Judith Underwood

1999

*
Building Reliable, High-Performance Communication Systems from Components *
| cite »

by Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, Robert L. Constable

1999

*
The Structure of Nuprl's Type Theory *
| cite »

by Robert L. Constable

1997

*
Formalizing Automata Theory I: Finite Automata *
| cite »

by Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe

1996

*
Formalizing Automata II: Decidable Properties *
| cite »

by Robert L. Constable, Pavel Naumov

1996

*
The Value of Automated Deduction *
| cite »

by Robert L. Constable

1996

*
Creating and Evaluating Interactive Formal Courseware for Mathematics and Computing *
| cite »

by Robert L. Constable

1996

*
Collaborative Mathematics Environments *
| cite »

by Robert L. Constable, Paul Chew, Keshav Pingali, Steve Vavasis, Richard Zippel

1996

*
Expressing Computational Complexity in Constructive Type Theory *
| cite »

by Robert L. Constable

1995

*
Experience Using Type Theory as a Foundation for Computer Science Circa 1985-1995 *
| cite »

by Robert L. Constable

1995

*
Towards Integrated Systems for Symbolic Algebra and Formal Constructive Mathematics *
| cite »

by Robert L. Constable, Paul B. Jackson

1994

*
Using Reflection to Explain and Enhance Type Theory *
| cite »

by Robert L. Constable

1994

*
Exporting and Reflecting Abstract Meta-mathematics *
| cite »

by Robert L. Constable

1994

*
Lectures on: Classical Proofs as Programs *
| cite »

by Robert L. Constable

1992

*
Metalevel Programming in Constructive Type Theory *
| cite »

by Robert L. Constable

1992

*
Formal Theories and Software Systems: Fundamental Connections Between Computer Science and Logic *
| cite »

by Robert L. Constable

1992

*
Metalogical Frameworks *
| cite »

by David A. Basin, Robert L. Constable

1991

*
Finding Computational Content from Classical Proofs *
| cite »

by Robert L. Constable, Chetan Murthy

1991

*
Type Theory as a Foundation for Computer Science *
| cite »

by Robert L. Constable

1991

*
The Semantics of Reflected Proof *
| cite »

by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken

1990

*
Reflecting the Open-Ended Computation System of Constructive Type Theory *
| cite »

by Robert L. Constable, Stuart F. Allen, Douglas J. Howe

1990

*
Nuprl as a General Logic *
| cite »

by Robert L. Constable, Douglas J. Howe

1990

*
Implementing Metamathematics as an Approach to Automatic Theorem Proving *
| cite »

by Robert L. Constable, Douglas J. Howe

1990

*
Assigning Meaning to Proofs: A Semantic Basis for Problem Solving Environments *
| cite »

by Robert L. Constable

1989

*
Computational Foundations of Basic Recursive Function Theory *
| cite »

by Robert L. Constable, Scott F. Smith

1988

*
Partial Objects in Constructive Type Theory *
| cite »

by Scott F. Smith, Robert L. Constable

1987

*
Implementing Mathematics with the Nuprl Development System *
| cite »

by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith

1986

*
Formalized Metareasoning in Type Theory *
| cite »

by Todd B. Knoblock, Robert L. Constable

1986

*
Infinite Objects in Type Theory *
| cite »

by Nax P. Mendler, Robert L. Constable, Prakash Panangaden

1986

*
Proofs as Programs *
| cite »

by Joseph L. Bates, Robert L. Constable

1985

*
Recursive Definitions in Type Theory *
| cite »

by Robert L. Constable, Nax P. Mendler

1985

*
Constructive Mathematics as a Programming Logic I: Some Principles of Theory *
| cite »

by Robert L. Constable

1985

*
Semantics of Evidence *
| cite »

by Robert L. Constable

1985

*
Writing Programs That Construct Proofs *
| cite »

by Robert L. Constable, Todd B. Knoblock, Joseph L. Bates

1984

*
A Hierarchical Approach to Formal Semantics With Application to the Definition of PL/ CS *
| cite »

by Robert L. Constable, James Donahue

July 01, 1979

*
A Programming Logic *
| cite »

by Robert L. Constable, Michael J. O'Donnell

1978

*
A Constructive Programming Logic *

by Robert L. Constable

August 08, 1977

*
Constructive Mathematics and Automatic Program Writers *
| cite »

by Robert L. Constable

1971

Crary, Karl

*
Computational Complexity and Induction for Partial Computable Functions in Type Theory *
| cite »

by Robert L. Constable, Karl Crary

2002

*
Type-Theoretic Methodology for Practical Programming Languages *
| cite »

by Karl Crary

1998

*
Foundations for the Implementation of Higher-Order Subtyping *
| cite »

by Karl Crary

1997

Cremer, J. F.

*
Implementing Mathematics with the Nuprl Development System *
| cite »

by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith

1986

Del Vecchio, Peter

*
Verification of Combinational Logic in Nuprl *
| cite »

by David A. Basin, Peter Del Vecchio

1989

Donahue, James

*
A Hierarchical Approach to Formal Semantics With Application to the Definition of PL/ CS *
| cite »

by Robert L. Constable, James Donahue

July 01, 1979

Eaton, Richard

*
Nuprl’s Inductive Logical Forms *

by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli

September 01, 2015

*
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

*
A Graph-Based Approach towards Discerning Inherent Structures in a Digital Library of Formal Mathematics. *
| cite »

by Lori Lorigo, Jon Kleinberg, Richard Eaton, Robert L. Constable

2004

*
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics *
| cite »

by Jon Kleinberg, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz

2003

*
FDL: A Prototype Formal Digital Library *

by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2002

*
The Nuprl Open Logical Environment *
| cite »

by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2000

Fluet, Matthew

*
Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations *
| cite »

by Stuart F. Allen, Robert L. Constable, Matthew Fluet

2004

Forester, Max B.

*
Formalizing Constructive Real Analysis *
| cite »

by Max B. Forester

1993

Gent, Ian

*
Search Algorithms in Type Theory *
| cite »

by James L. Caldwell, Ian Gent, Judith Underwood

2000

Geser, Alfons

*
Termination of Single-Threaded One-rule Semi-Thue Systems *
| cite »

by Wojciech Moczydlowski, Alfons Geser

2005

Giunchiglia, Fausto

*
Reflection in Constructive and Non-Constructive Automated Reasoning *
| cite »

by Fausto Giunchiglia, Alan Smaill

1989

Griffin, Timothy G.

*
Notational Definition and Top-down Refinement for Interactive Proof Development Systems *
| cite »

by Timothy G. Griffin

1988

Guaspari, David

*
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

*
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML *

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

September 01, 2015

*
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems *

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

March 31, 2013

*
Generating Event Logics with Higher-Order Processes as Realizers *
| cite »

by Mark Bickford, Robert L. Constable, David Guaspari

2010

*
Encoding Pi Calculus *
| cite »

by David Guaspari

2010

*
Formalizing chain replication *

by Mark Bickford, David Guaspari

2006

*
A Programming Logic for Distributed Systems *
| cite »

by Mark Bickford, David Guaspari

2005

Hafizogullari, Ozan

*
Dependence Analysis Through Type Inference *
| cite »

by Ozan Hafizogullari, Christoph Kreitz

1999

Halpern, Joseph Y.

*
Knowledge-based synthesis of distributed systems using event structures *
| cite »

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

2005

*
Knowledge-Based Synthesis of Distributed Systems Using Event Structures *

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

2004

Harmelen, Frank Van

*
The Oyster-Clam System *
| cite »

by Alan Bundy, Frank Van Harmelen, Christian Horn, Alan Smaill

1990

Harper, Robert W.

*
Implementing Mathematics with the Nuprl Development System *
| cite »

by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith

1986

*
Aspects of the Implementation of Type Theory *
| cite »

by Robert W. Harper

1985

Hayden, Mark

*
The Horus and Ensemble Projects: Accomplishments and Limitations *
| cite »

by Kenneth Birman, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, Werner Vogels

2000

*
Building Reliable, High-Performance Communication Systems from Components *
| cite »

by Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, Robert L. Constable

1999

*
The Ensemble System *
| cite »

by Mark Hayden

1998

*
A Proof Environment for the Development of Group Communication Systems *
| cite »

by Christoph Kreitz, Mark Hayden, Jason Hickey

1998

Hickey, Jason

*
MetaPRL -- A Modular Logical Environment *
| cite »

by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo

2003

*
Formal Compiler Implementation in a Logical Framework *
| cite »

by Jason Hickey, Aleksey Nogin

2003

*
The MetaPRL Logical Programming Environment *
| cite »

by Jason Hickey

2001

*
The Horus and Ensemble Projects: Accomplishments and Limitations *
| cite »

by Kenneth Birman, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, Werner Vogels

2000

*
Nuprl's Class Theory and Its Applications *
| cite »

by Robert L. Constable, Jason Hickey

2000

*
Fast Tactic-Based Theorem Proving *
| cite »

by Jason Hickey, Aleksey Nogin

2000

*
An Object-Oriented Approach to Verifying Group Communication Systems *
| cite »

by Mark Bickford, Jason Hickey

1999

*
Fault-Tolerant Distributed Theorem Proving *
| cite »

by Jason Hickey

1999

*
Specifications and Proofs for Ensemble Layers *
| cite »

by Jason Hickey, Nancy Lynch, Robbert van Renesse

1999

*
Building Reliable, High-Performance Communication Systems from Components *
| cite »

by Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, Robert L. Constable

1999

*
A Proof Environment for the Development of Group Communication Systems *
| cite »

by Christoph Kreitz, Mark Hayden, Jason Hickey

1998

*
Nuprl-Light: An Implementation Framework for Higher-Order Logics *
| cite »

by Jason Hickey

1997

*
A Semantics of Objects in Type Theory *
| cite »

by Jason Hickey

1997

*
Formal Objects in Type Theory Using Very Dependent Types *
| cite »

by Jason Hickey

1996

*
Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization *
| cite »

by John O'Leary, Miriam Leeser, Jason Hickey, Mark Aagaard

1994

Ho, Chi

*
Byzantine Chain Replication *
| cite »

by Robbert van Renesse, Chi Ho, Nicolas Schiper

December 20, 2012

Holland-Minkley, Amanda

*
Planning Proof Content for Communicating Induction *
| cite »

by Amanda Holland-Minkley

2002

*
Verbalization of High-Level Formal Proofs *
| cite »

by Amanda Holland-Minkley, Regina Barzilay, Robert L. Constable

1999

Horn, Christian

*
The Oyster-Clam System *
| cite »

by Alan Bundy, Frank Van Harmelen, Christian Horn, Alan Smaill

1990

*
The Nuprl Proof Development System *
| cite »

by Christian Horn

1988

Howe, Douglas J.

*
A type annotation scheme for Nuprl *
| cite »

by Douglas J. Howe

October 01, 1998

*
Semantic Foundations for Embedding HOL in Nuprl *
| cite »

by Douglas J. Howe

1996

*
Importing Mathematics from HOL into Nuprl *
| cite »

by Douglas J. Howe

1996

*
An Operational Approach to Combining Classical Set Theory and Functional Programming Languages *
| cite »

by Douglas J. Howe, Scott D. Stoller

1994

*
Reasoning About Functional Programs in Nuprl *
| cite »

by Douglas J. Howe

1993

*
A Simple Type Theory for Reasoning About Functional Programs *
| cite »

by Douglas J. Howe

1992

*
Some Normalization Properties of Martin-Lof's Type Theory and Applications *
| cite »

by David A. Basin, Douglas J. Howe

1991

*
On computational open-endedness in Martin-Lof's type theory *

by Douglas J. Howe

July 15, 1991

*
The Semantics of Reflected Proof *
| cite »

by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken

1990

*
Reflecting the Open-Ended Computation System of Constructive Type Theory *
| cite »

by Robert L. Constable, Stuart F. Allen, Douglas J. Howe

1990

*
Nuprl as a General Logic *
| cite »

by Robert L. Constable, Douglas J. Howe

1990

*
Implementing Metamathematics as an Approach to Automatic Theorem Proving *
| cite »

by Robert L. Constable, Douglas J. Howe

1990

*
Equality in Lazy Computation Systems *
| cite »

by Douglas J. Howe

1989

*
Automating Reasoning in an Implementation of Constructive Type Theory *
| cite »

by Douglas J. Howe

1988

*
Computational Metatheory in Nuprl *
| cite »

by Douglas J. Howe

1988

*
The Computational Behaviour of Girard's Paradox *
| cite »

by Douglas J. Howe

1987

*
Implementing Number Theory: An Experiment with Nuprl *
| cite »

by Douglas J. Howe

1987

*
Implementing Mathematics with the Nuprl Development System *
| cite »

by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith

1986

Jackson, Paul B.

*
Formalizing Automata Theory I: Finite Automata *
| cite »

by Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe

1996

*
The Nuprl Proof Development System, Version 4.2 Reference Manual and User's Guide *
| cite »

by Paul B. Jackson

1996

*
Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra *
| cite »

by Paul B. Jackson

1995

*
Towards Integrated Systems for Symbolic Algebra and Formal Constructive Mathematics *
| cite »

by Robert L. Constable, Paul B. Jackson

1994

*
Exploring Abstract Algebra in Constructive Type Theory *
| cite »

by Paul B. Jackson

1994

*
Nuprl and Its Use in Circuit Design *
| cite »

by Paul B. Jackson

1992

*
Developing a Toolkit for Floating-Point Hardware in the Nuprl Proof Development System *
| cite »

by Paul B. Jackson

1991

*
Logic-Based Knowledge Representation *
| cite »

by Paul B. Jackson

1989

Kamareddine, Fairouz

*
Russell's Orders in Kripke's Theory of Truth and Computational Type Theory *
| cite »

by Robert L. Constable, Fairouz Kamareddine, Twan Laan

2012

Kellison, Ariel

*
Implementing Euclid's Straightedge and Compass Constructions in Type Theory *
| cite »

by Ariel Kellison, Mark Bickford, Robert L. Constable

2018

Kleinberg, Jon

*
A Graph-Based Approach towards Discerning Inherent Structures in a Digital Library of Formal Mathematics. *
| cite »

by Lori Lorigo, Jon Kleinberg, Richard Eaton, Robert L. Constable

2004

*
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics *
| cite »

by Jon Kleinberg, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz

2003

Knoblock, Todd B.

*
Metamathematical Extensibility in Type Theory *
| cite »

by Todd B. Knoblock

1987

*
Implementing Mathematics with the Nuprl Development System *
| cite »

by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith

1986

*
Formalized Metareasoning in Type Theory *
| cite »

by Todd B. Knoblock, Robert L. Constable

1986

*
Writing Programs That Construct Proofs *
| cite »

by Robert L. Constable, Todd B. Knoblock, Joseph L. Bates

1984

Kopylov, Alexei

*
Type Theoretical Foundations for Data Structures, Classes, and Objects *
| cite »

by Alexei Kopylov

2004

*
Dependent Intersection: A New Way of Defining Records in Type Theory *
| cite »

by Alexei Kopylov

2003

*
Markov's Principle For Propositional Type Theory *
| cite »

by Alexei Kopylov, Aleksey Nogin

2001

Kozen, Dexter

*
Automating Proofs in Category Theory *
| cite »

by Dexter Kozen, Christoph Kreitz, Eva Richter

2006

Kreitz, Christoph

*
Nuprl as Logical Framework for Automating Proofs in Category *
| cite »

by Christoph Kreitz

April 26, 2012

*
Introduction to Classic ML *
| cite »

by Christoph Kreitz, Vincent Rahli

2011

*
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

*
Automating Proofs in Category Theory *
| cite »

by Dexter Kozen, Christoph Kreitz, Eva Richter

2006

*
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics *
| cite »

by Jon Kleinberg, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz

2003

*
The FDL Navigator: Browsing and Manipulating Formal Content *
| cite »

by Christoph Kreitz

2003

*
FDL: A Prototype Formal Digital Library *

by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2002

*
An Experiment in Formal Design Using Meta-Properties *
| cite »

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

2001

*
Proving Hybrid Protocols Correct *
| cite »

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

2001

*
Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment *
| cite »

by Mark Bickford, Christoph Kreitz, Robbert van Renesse

2001

*
Connection-Driven Inductive Theorem Proving *
| cite »

by Christoph Kreitz, Brigitte Pientka

2001

*
Protocol Switching: Exploiting Meta-Properties *
| cite »

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

2001

*
JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants *
| cite »

by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin

2001

*
The Nuprl Open Logical Environment *
| cite »

by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2000

*
The Horus and Ensemble Projects: Accomplishments and Limitations *
| cite »

by Kenneth Birman, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, Werner Vogels

2000

*
Matrix-Based Constructive Theorem Proving *
| cite »

by Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka

2000

*
Matrix-Based Inductive Theorem Proving *
| cite »

by Christoph Kreitz, Brigitte Pientka

2000

*
A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems *
| cite »

by Christoph Kreitz, Stephan Schmitt

2000

*
Dependence Analysis Through Type Inference *
| cite »

by Ozan Hafizogullari, Christoph Kreitz

1999

*
Connection-Based Theorem Proving in Classical and Non-Classical Logics *
| cite »

by Christoph Kreitz, Jens Otten

1999

*
Automated Fast-Track Reconfiguration of Group Communication Systems *
| cite »

by Christoph Kreitz

1999

*
Automating Inductive Specification Proofs *
| cite »

by Brigitte Pientka, Christoph Kreitz

1999

*
Building Reliable, High-Performance Communication Systems from Components *
| cite »

by Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, Robert L. Constable

1999

*
A Proof Environment for the Development of Group Communication Systems *
| cite »

by Christoph Kreitz, Mark Hayden, Jason Hickey

1998

*
Formal Reasoning About Communication Systems II: Automated Fast-Track Reconfiguration *
| cite »

by Christoph Kreitz

1998

*
A Matrix Characterization for MELL *
| cite »

by Heiko Mantel, Christoph Kreitz

1998

*
Instantiation of Existentially Quantified Variables in Inductive Specification Proofs *
| cite »

by Brigitte Pientka, Christoph Kreitz

1998

*
Formal Reasoning About Communication Systems I: Embedding ML in Type Theory *
| cite »

by Christoph Kreitz

1997

*
Meta-Synthesis: Deriving Programs That Develop Programs *
| cite »

by Christoph Kreitz

1992

*
Constructive Automata Theory Implemented with the Nuprl Proof Development System *
| cite »

by Christoph Kreitz

1986

Laan, Twan

*
Russell's Orders in Kripke's Theory of Truth and Computational Type Theory *
| cite »

by Robert L. Constable, Fairouz Kamareddine, Twan Laan

2012

Leeser, Miriam

*
Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization *
| cite »

by John O'Leary, Miriam Leeser, Jason Hickey, Mark Aagaard

1994

*
Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification *
| cite »

by Mark Aagaard, Miriam Leeser

1993

*
Using Nuprl for the Verification and Synthesis of Hardware *
| cite »

by Miriam Leeser

1992

*
Formally Verified Synthesis of Combinational Circuits *
| cite »

by David A. Basin, Geoffrey Brown, Miriam Leeser

1991

Liu, Xiaoming

*
Proving Hybrid Protocols Correct *
| cite »

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

2001

*
Protocol Switching: Exploiting Meta-Properties *
| cite »

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

2001

*
Building Reliable, High-Performance Communication Systems from Components *
| cite »

by Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, Robert L. Constable

1999

Lorigo, Lori

*
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

*
Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts *
| cite »

by Stuart F. Allen, Robert L. Constable, Lori Lorigo

2006

*
Information Management in the Service of Knowledge and Discovery *
| cite »

by Lori Lorigo

2006

by Lori Lorigo, Jon Kleinberg, Richard Eaton, Robert L. Constable

2004

*
MetaPRL -- A Modular Logical Environment *
| cite »

by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo

2003

*
FDL: A Prototype Formal Digital Library *

by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2002

*
JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants *
| cite »

by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin

2001

*
The Nuprl Open Logical Environment *
| cite »

by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo

2000

Lynch, Nancy

*
Specifications and Proofs for Ensemble Layers *
| cite »

by Jason Hickey, Nancy Lynch, Robbert van Renesse

1999

Madden, Peter

*
Automatic Program Optimization Via the Transformation of Nuprl Synthesis Proofs *
| cite »

by Peter Madden

1988

Mantel, Heiko

*
A Matrix Characterization for MELL *
| cite »

by Heiko Mantel, Christoph Kreitz

1998

Mendler, Nax P.

*
Inductive Definition in Type Theory *
| cite »

by Nax P. Mendler

1988

*
Recursive Types and Type Constraints in Second-Order Lambda Calculus *
| cite »

by Nax P. Mendler

1987

*
Implementing Mathematics with the Nuprl Development System *
| cite »

by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith

1986

*
Infinite Objects in Type Theory *
| cite »

by Nax P. Mendler, Robert L. Constable, Prakash Panangaden

1986

*
Recursive Definitions in Type Theory *
| cite »

by Robert L. Constable, Nax P. Mendler

1985

Moczydlowski, Wojciech

*
Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus *
| cite »

by Wojciech Moczydlowski, Robert L. Constable

2007

*
A Dependent Set Theory *

by Wojciech Moczydlowski

2007

*
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics *
| cite »

by Robert L. Constable, Wojciech Moczydlowski

2006

*
A Normalizing Intuitionistic Set Theory with Inaccessible Sets *
| cite »

by Wojciech Moczydlowski

2006

*
Normalization of intuitionistic set theories. *
| cite »

by Wojciech Moczydlowski

2006

*
Termination of Single-Threaded One-rule Semi-Thue Systems *
| cite »

by Wojciech Moczydlowski, Alfons Geser

2005

Moran, Evan

*
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

Moschovakis, Joan Rand

*
Intuitionistic Mathematics and Logic *

by Joan Rand Moschovakis, Garyfallia Vafeiadou

January 25, 2020

Moten, Roderick

*
Concurrent Refinement in Nuprl *
| cite »

by Roderick Moten

1997

Murthy, Chetan

*
A Computational Analysis of Girard's Translation and LC *
| cite »

by Chetan Murthy

1992

*
Finding Computational Content from Classical Proofs *
| cite »

by Robert L. Constable, Chetan Murthy

1991

*
An Evaluation Semantics for Classical Proofs *
| cite »

by Chetan Murthy

1991

*
A Constructive Proof of Higman's Lemma *
| cite »

by Chetan Murthy, James R. Russell

1990

*
Extracting Constructive Content from Classical Proofs *
| cite »

by Chetan Murthy

1990

Naumov, Pavel

*
Formalizing Reference Types in Nuprl *
| cite »

by Pavel Naumov

1998

*
Formalizing Automata Theory I: Finite Automata *
| cite »

by Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe

1996

*
Formalizing Automata II: Decidable Properties *
| cite »

by Robert L. Constable, Pavel Naumov

1996

Nogin, Aleksey

*
MetaPRL -- A Modular Logical Environment *
| cite »

by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo

2003

*
Formal Compiler Implementation in a Logical Framework *
| cite »

by Jason Hickey, Aleksey Nogin

2003

*
Quotient Types: A Modular Approach *
| cite »

by Aleksey Nogin

2002

*
Markov's Principle For Propositional Type Theory *
| cite »

by Alexei Kopylov, Aleksey Nogin

2001

*
Writing Constructive Proofs Yielding Efficient Extracted Programs *
| cite »

by Aleksey Nogin

2001

*
JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants *
| cite »

by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin

2001

*
Fast Tactic-Based Theorem Proving *
| cite »

by Jason Hickey, Aleksey Nogin

2000

O'Donnell, Michael J.

*
A Programming Logic *
| cite »

by Robert L. Constable, Michael J. O'Donnell

1978

O'Leary, John

*
Non-Restoring Integer Square Root: A Case Study in Design by Principled Optimization *
| cite »

by John O'Leary, Miriam Leeser, Jason Hickey, Mark Aagaard

1994

Otten, Jens

*
Matrix-Based Constructive Theorem Proving *
| cite »

by Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka

2000

*
Connection-Based Theorem Proving in Classical and Non-Classical Logics *
| cite »

by Christoph Kreitz, Jens Otten

1999

Panangaden, Prakash

*
Implementing Mathematics with the Nuprl Development System *
| cite »

by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith

1986

*
Infinite Objects in Type Theory *
| cite »

by Nax P. Mendler, Robert L. Constable, Prakash Panangaden

1986

Petride, Sabina

*
Knowledge-based synthesis of distributed systems using event structures *
| cite »

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

2005

*
Knowledge-Based Synthesis of Distributed Systems Using Event Structures *

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

2004

Pientka, Brigitte

*
Connection-Driven Inductive Theorem Proving *
| cite »

by Christoph Kreitz, Brigitte Pientka

2001

*
Matrix-Based Constructive Theorem Proving *
| cite »

by Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka

2000

*
Matrix-Based Inductive Theorem Proving *
| cite »

by Christoph Kreitz, Brigitte Pientka

2000

*
Automating Inductive Specification Proofs *
| cite »

by Brigitte Pientka, Christoph Kreitz

1999

*
Instantiation of Existentially Quantified Variables in Inductive Specification Proofs *
| cite »

by Brigitte Pientka, Christoph Kreitz

1998

Pingali, Keshav

*
Collaborative Mathematics Environments *
| cite »

by Robert L. Constable, Paul Chew, Keshav Pingali, Steve Vavasis, Richard Zippel

1996

Rahli, Vincent

*
Open Bar -- A Reconciliation between Intuitionistic and Classical Logic *

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

2020

*
Bar Induction is Compatible with Constructive Type Theory *
| cite »

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

2019

*
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

*
A Verified Theorem Prover Backend Supported by a Monotonic Library *
| cite »

by Vincent Rahli, Liron Cohen, Mark Bickford

November 01, 2018

*
Bar Induction: The Good, the Bad, and the Ugly *
| cite »

by Vincent Rahli, Mark Bickford, Robert L. Constable

April 11, 2017

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

November 15, 2017

*
A Nominal Exploration of Intuitionism *

by Vincent Rahli, Mark Bickford

January 18, 2016

*
Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML *

by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable

September 01, 2015

*
Coq as a Metatheory for Nuprl with Bar Induction *

by Vincent Rahli, Mark Bickford

September 14, 2015

*
Nuprl’s Inductive Logical Forms *

by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli

September 01, 2015

*
Developing Correctly Replicated Databases Using Formal Tools *

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

June 23, 2014

*
A Type Theory with Partial Equivalence Relations as Types *

by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli

May 12, 2014

*
Towards a Formally Verified Proof Assistant *

by Abhishek Anand, Vincent Rahli

July 14, 2014

*
A Generic Approach to Proofs about Substitution *

by Abhishek Anand, Vincent Rahli

July 17, 2014

*
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

*
The Logic of Events, a framework to reason about distributed systems *
| cite »

by Mark Bickford, Vincent Rahli, Robert L. Constable

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

*
Interfacing with Proof Assistants for Domain Specific Programming Using EventML *
| cite »

by Vincent Rahli

July 11, 2012

*
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

*
Investigations in intersection types:Confluence, and semantics of expansion in the lambda-calculus, and a type error slicing method *
| cite »

by Vincent Rahli

2011

*
Introduction to Classic ML *
| cite »

by Christoph Kreitz, Vincent Rahli

2011

Richter, Eva

*
Automating Proofs in Category Theory *
| cite »

by Dexter Kozen, Christoph Kreitz, Eva Richter

2006

Rodeh, Ohad

*
The Horus and Ensemble Projects: Accomplishments and Limitations *
| cite »

by Kenneth Birman, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, Werner Vogels

2000

Rowe, Reuben

*
Automated Reasoning in Herbrand Structures *

by Liron Cohen, Reuben Rowe, Yoni Zohar

June 03, 2019

*
Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent *
| cite »

by Liron Cohen, Reuben Rowe

July 01, 2018

Russell, James R.

*
A Constructive Proof of Higman's Lemma *
| cite »

by Chetan Murthy, James R. Russell

1990

Sasaki, James T.

*
Implementing Mathematics with the Nuprl Development System *
| cite »

by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith

1986

*
Extracting Efficient Code from Constructive Proofs *
| cite »

by James T. Sasaki

1985

Schiper, Nicolas

*
Developing Correctly Replicated Databases Using Formal Tools *

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

June 23, 2014

*
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

*
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

*
Byzantine Chain Replication *
| cite »

by Robbert van Renesse, Chi Ho, Nicolas Schiper

December 20, 2012

Schmitt, Stephan

*
JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants *
| cite »

by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin

2001

*
Matrix-Based Constructive Theorem Proving *
| cite »

by Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka

2000

*
A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems *
| cite »

by Christoph Kreitz, Stephan Schmitt

2000

Sernaker, Sarah

*
A Formal Exploration of Constructive Geometry *

by Robert L. Constable, Sarah Sernaker

2016

Smaill, Alan

*
The Oyster-Clam System *
| cite »

by Alan Bundy, Frank Van Harmelen, Christian Horn, Alan Smaill

1990

*
Reflection in Constructive and Non-Constructive Automated Reasoning *
| cite »

by Fausto Giunchiglia, Alan Smaill

1989

Smith, Scott F.

*
Partial Objects in Type Theory *
| cite »

by Scott F. Smith

1989

*
Computational Foundations of Basic Recursive Function Theory *
| cite »

by Robert L. Constable, Scott F. Smith

1988

*
Partial Objects in Constructive Type Theory *
| cite »

by Scott F. Smith, Robert L. Constable

1987

*
Implementing Mathematics with the Nuprl Development System *
| cite »

by Robert L. Constable, Stuart F. Allen, H. M. Bromley, Walter Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith

1986

Stoller, Scott D.

*
An Operational Approach to Combining Classical Set Theory and Functional Programming Languages *
| cite »

by Douglas J. Howe, Scott D. Stoller

1994

Underwood, Judith

*
Search Algorithms in Type Theory *
| cite »

by James L. Caldwell, Ian Gent, Judith Underwood

2000

*
Metalogical Frameworks II: Developing a Reflected Decision Procedure *
| cite »

by William Aitken, Robert L. Constable, Judith Underwood

1999

*
Classical Tools for Constructive Proof Search *
| cite »

by James L. Caldwell, Judith Underwood

1996

*
Aspects of the Computational Content of Proofs *
| cite »

by Judith Underwood

1994

*
The Tableau Algorithm for Intuitionistic Propositional Calculus as a Constructive Completeness Proof *
| cite »

by Judith Underwood

1993

*
A Constructive Completeness Proof for the Intuitionistic Propositional Calculus *
| cite »

by Judith Underwood

1990

Uribe, Juan

*
Formalizing Automata Theory I: Finite Automata *
| cite »

by Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe

1996

Vafeiadou, Garyfallia

*
Intuitionistic Mathematics and Logic *

by Joan Rand Moschovakis, Garyfallia Vafeiadou

January 25, 2020

van Renesse, Robbert

*
Developing Correctly Replicated Databases Using Formal Tools *

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

June 23, 2014

*
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

*
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

*
Byzantine Chain Replication *
| cite »

by Robbert van Renesse, Chi Ho, Nicolas Schiper

December 20, 2012

*
Investigating Correct-by-Construction Attack-Tolerant Systems *
| cite »

by Robert L. Constable, Mark Bickford, Robbert van Renesse

2010

*
An Experiment in Formal Design Using Meta-Properties *
| cite »

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

2001

*
Proving Hybrid Protocols Correct *
| cite »

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

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

*
The Horus and Ensemble Projects: Accomplishments and Limitations *
| cite »

by Kenneth Birman, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, Werner Vogels

2000

*
Specifications and Proofs for Ensemble Layers *
| cite »

by Jason Hickey, Nancy Lynch, Robbert van Renesse

1999

*
Building Reliable, High-Performance Communication Systems from Components *
| cite »

by Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, Robert L. Constable

1999

Vavasis, Steve

*
Collaborative Mathematics Environments *
| cite »

by Robert L. Constable, Paul Chew, Keshav Pingali, Steve Vavasis, Richard Zippel

1996

Vogels, Werner

*
The Horus and Ensemble Projects: Accomplishments and Limitations *
| cite »

by Kenneth Birman, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, Werner Vogels

2000

Zippel, Richard

*
Collaborative Mathematics Environments *
| cite »

by Robert L. Constable, Paul Chew, Keshav Pingali, Steve Vavasis, Richard Zippel

1996

Zohar, Yoni

*
Automated Reasoning in Herbrand Structures *

by Liron Cohen, Reuben Rowe, Yoni Zohar

June 03, 2019