PRL Home Introduction Math Library Publications Projects System

Seminar People The Book Lectures Other Groups

Knowledge Base of
Publications, Seminars, & Math Library

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

Browse by author | title | year | subject

List by Author

1030 results

Aagaard, Mark

Publication 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

Seminar Verifying a Pipelined Circuit
by Mark Aagaard
April 05, 1994

Publication Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification | cite »
by Mark Aagaard, Miriam Leeser
1993

Seminar Using Reflection to External Automated Theorem Provers
by Mark Aagaard
March 30, 1993

Seminar HOL Workshop
by Mark Aagaard
September 15, 1992

Aitken, William

Publication Metalogical Frameworks II: Developing a Reflected Decision Procedure | cite »
by William Aitken, Robert L. Constable, Judith Underwood
1999

Seminar Reflection
by William Aitken
April 06, 1993

Seminar Reflection 2
by William Aitken, William Aitken
March 05, 1992

Seminar Reflection 2
by William Aitken, William Aitken
February 18, 1992

Seminar A Basis for Constructive, Reflexive Type Theory
by William Aitken
October 01, 1990

Publication The Semantics of Reflected Proof | cite »
by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken
1990

Allen, Stuart F.

Publication 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

Publication Enabling Large Scale Coherency Among Mathematical Texts | cite »
by Stuart F. Allen, Robert L. Constable
2006

Publication Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts | cite »
by Stuart F. Allen, Robert L. Constable, Lori Lorigo
2006

Publication An Abstract Semantics for Atoms in Nuprl | cite »
by Stuart F. Allen
2006

Seminar A Semantics for Abstract Atoms in Nuprl
by Stuart F. Allen
March 31, 2006

Seminar Anchoring Expository Text in Formal Mathematics -- Part II
by Stuart F. Allen
April 15, 2005

Seminar Anchoring Expository Text in Formal Mathematics
by Stuart F. Allen
December 06, 2004

Publication 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

Math Book Square Root of 2 is Irrational
by Stuart F. Allen
August 04, 2004

Math Book Fundamental Theorem of Arithmetic
by Stuart F. Allen
August 02, 2004

Math Book Iterated Binary Operations
by Stuart F. Allen
August 02, 2004

Math Book Russel's Paradox
by Stuart F. Allen
December 14, 2004

Math Book How to browse the library
by Stuart F. Allen
December 14, 2004

Publication Abstract Identifiers, Intertextual Reference and a Computational Basis for Recordkeeping | cite »
by Stuart F. Allen
2004

Math Book Towers of Hanoi
by Stuart F. Allen
April 27, 2004

Math Book Readability Exercise (num theory)
by Stuart F. Allen
December 14, 2004

Math Book Discrete Math Materials
by Stuart F. Allen
August 02, 2004

Seminar Type Theory as a Legacy from Logicism
by Stuart F. Allen
March 08, 2004

Seminar Applied Logic as Part of an Effort to Accumulate Precise Knowledge
by Stuart F. Allen
February 09, 2004

Seminar Remarks on the FDL (Formal Digital Library) Project -- Continuation of talk begun November 17
by Stuart F. Allen
December 01, 2003

Seminar Remarks on the FDL (Formal Digital Library) Project
by Stuart F. Allen
November 17, 2003

Math Book Nuprl Basics
by Stuart F. Allen
September 18, 2003

Math Book Standard Resources
by Stuart F. Allen
September 23, 2003

Math Book Elementary Number Theory
by Stuart F. Allen
September 23, 2003

Publication Practical Reflection in Nuprl | cite »
by Eli Barzilay, Stuart F. Allen, Robert L. Constable
2003

Math Book Nuprl Editor and Interface
by Stuart F. Allen
September 23, 2003

Publication Abstract Identifiers and Textual Reference | cite »
by Stuart F. Allen
2002

Publication Reflecting Higher-Order Abstract Syntax in Nuprl | cite »
by Eli Barzilay, Stuart F. Allen
2002

Publication FDL: A Prototype Formal Digital Library
by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2002

Seminar Report on the Design of the Formal Digital Library
by Richard Eaton, Robert L. Constable, Stuart F. Allen
April 08, 2002

Seminar Explaining the Formal Digital Library
by Stuart F. Allen, Robert L. Constable, Richard Eaton
March 11, 2002

Seminar Progress on the ONR University Research Initiative in Digital Libraries for Computational Mathematics
by Stuart F. Allen, Robert L. Constable
December 03, 2001

Publication Logical Aspects of Digital Mathematics Libraries (extended abstract) | cite »
by Stuart F. Allen, James L. Caldwell, Robert L. Constable
2001

Math Book Lists
by Stuart F. Allen
May 15, 2001

Seminar 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

Publication The Nuprl Open Logical Environment | cite »
by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2000

Seminar Semantics and Pragmatics of Reflected Proof
by Stuart F. Allen, Sergei Artemov, Robert L. Constable
December 01, 1998

Seminar Some Uses of the Intersection Type
by Stuart F. Allen, Robert L. Constable
May 03, 1999

Seminar Using Nuprl as a Formal Assistant for Preparing Largely Informal Material
by Stuart F. Allen
March 29, 1999

Seminar Reflection Mechanisms in Nuprl
by Stuart F. Allen, Robert L. Constable
November 10, 1998

Publication From dy/dx to []P: A Matter of Notation | cite »
by Stuart F. Allen
1998

Seminar Application of Notational Methods in dy/dx
by Stuart F. Allen
March 31, 1998

Seminar Abstract Identifiers in Nuprl 5 (continued)
by Stuart F. Allen
October 28, 1997

Seminar Abstract Identifiers in Nuprl 5
by Stuart F. Allen
October 21, 1997

Seminar Discussion of Issues in Logic Library Design
by Robert L. Constable, Jason Hickey, Stuart F. Allen, Richard Eaton
March 03, 1997

Seminar Designing a Logical Library
by Stuart F. Allen
February 24, 1997

Seminar New Nuprl Editor
by Stuart F. Allen
November 07, 1995

Seminar Overview of Nuprl 5
by Stuart F. Allen
September 19, 1995

Seminar Imperative Program Semantics
by Stuart F. Allen
May 02, 1995

Seminar The "Interface" Version of Nuprl
by Stuart F. Allen, Richard Eaton
November 15, 1994

Seminar Reasoning about Scientific Programs
by Conal Mannion, Stuart F. Allen
1993-1994

Seminar Polya/Nuprl
by Stuart F. Allen
1993-1994

Seminar Editing
by Stuart F. Allen
November 16, 1993

Seminar Attaching Context to Objects in the Library
by Stuart F. Allen
February 04, 1992

Seminar PRL Library Day
by Stuart F. Allen
November 19, 1991

Publication The Semantics of Reflected Proof | cite »
by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken
1990

Publication Reflecting the Open-Ended Computation System of Constructive Type Theory | cite »
by Robert L. Constable, Stuart F. Allen, Douglas J. Howe
1990

Seminar Continuation of A Type Theoretic Interpretation of DougHowe's Squiggle Relation
by Stuart F. Allen
April 26, 1988

Seminar A Type Theoretic Interpretation of Doug Howe's Squiggle Relation
by Stuart F. Allen
April 19, 1988

Publication A Non-Type-Theoretic Definition of Martin-Lof's Types | cite »
by Stuart F. Allen
1987

Publication A Non-Type-Theoretic Semantics for Type-Theoretic Language | cite »
by Stuart F. Allen
1987

Publication 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

Seminar Prolog
by Ryan Stansifer, Stuart F. Allen
1984-1985

Seminar Predicate Calculus Model
by Stuart F. Allen
1984-1985

Anand, Abhishek

Seminar Topics in Type Theory
by Abhishek Anand, Robert L. Constable, Mark Bickford
October 22, 2014

Seminar Coinduction in Coq
by Abhishek Anand
November 12, 2014

Seminar From Replicated Databases to Ensembles of Collaborating Robots
by Abhishek Anand, Mark Bickford
November 19, 2014

Publication A Type Theory with Partial Equivalence Relations as Types
by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli
May 12, 2014

Publication Towards a Formally Verified Proof Assistant
by Abhishek Anand, Vincent Rahli
July 14, 2014

Publication A Generic Approach to Proofs about Substitution
by Abhishek Anand, Vincent Rahli
July 17, 2014

Publication Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types | cite »
by Vincent Rahli, Mark Bickford, Abhishek Anand
April 22, 2013

Seminar The Beauty of Nuprl's Uniform Term Representation and How to Reason about those Terms in Coq
by Abhishek Anand
October 09, 2013

Seminar A verified proof assistant
by Vincent Rahli, Abhishek Anand
October 30, 2013

Seminar How far can we go with Induction-Recursion?
by Abhishek Anand, Vincent Rahli
November 20, 2013

Seminar The Type Base and Undecidability in Type Theory
by Abhishek Anand
September 21, 2012

Seminar Bar Induction and the Fan Theorem in Constructive Type Theory
by Robert L. Constable, Mark Bickford, Abhishek Anand
October 12, 2012

Artemov, Sergei

Seminar Reflected Lambda Calculus
by Sergei Artemov
October 02, 2000

Seminar Stability of intuitionistic systems
by Sergei Artemov
April 24, 2000

Seminar Semantics and Pragmatics of Reflected Proof
by Stuart F. Allen, Sergei Artemov, Robert L. Constable
December 01, 1998

Seminar On the Reflection Mechanism in Nuprl
by Sergei Artemov
November 24, 1998

Seminar Proof Polynomials: Cut Elimination
by Sergei Artemov
October 07, 1997

Seminar Operational Modal Logic
by Sergei Artemov
January 29, 1996

Aydemir, Brian

Publication MetaPRL -- A Modular Logical Environment | cite »
by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo
2003

Barzilay, Eli

Publication Implementing Reflection in Nuprl | cite »
by Eli Barzilay
2006

Publication Practical Reflection in Nuprl | cite »
by Eli Barzilay, Stuart F. Allen, Robert L. Constable
2003

Publication MetaPRL -- A Modular Logical Environment | cite »
by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo
2003

Publication Reflecting Higher-Order Abstract Syntax in Nuprl | cite »
by Eli Barzilay, Stuart F. Allen
2002

Publication Quotation and Reflection in Nuprl and Scheme | cite »
by Eli Barzilay
2001

Seminar Reflection in First-Order Logic
by Eli Barzilay
February 12, 2001

Seminar Latest results about reflection (TENTATIVE)
by Eli Barzilay
November 20, 2000

Seminar Reflection Part II
by Eli Barzilay
April 03, 2000

Seminar Analysis of reflection in programming languages using Scheme as the main example
by Eli Barzilay
March 06, 2000

Seminar Practical Uses of Quotations, Macros and Reflection
by Eli Barzilay
April 05, 1999

Barzilay, Regina

Seminar HOAS -- Higher Order Abstract Syntax: a Survey
by Regina Barzilay
October 21, 2002

Seminar Online Demonstration of Syntactic Reflection. Realizing an Argument about Syntax (Tarski).
by Regina Barzilay
March 03, 2003

Seminar The Abstract Term Type
by Regina Barzilay
March 04, 2002

Publication Verbalization of High-Level Formal Proofs | cite »
by Amanda Holland-Minkley, Regina Barzilay, Robert L. Constable
1999

Basin, David A.

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
May 04, 1993

Publication Extracting Circuits from Constructive Proofs | cite »
by David A. Basin
1991

Publication Formally Verified Synthesis of Combinational Circuits | cite »
by David A. Basin, Geoffrey Brown, Miriam Leeser
1991

Publication Metalogical Frameworks | cite »
by David A. Basin, Robert L. Constable
1991

Publication Some Normalization Properties of Martin-Lof's Type Theory and Applications | cite »
by David A. Basin, Douglas J. Howe
1991

Publication Building Problem Solving Environments in Constructive Type Theory | cite »
by David A. Basin
1990

Publication Building Theories in Nuprl | cite »
by David A. Basin
1989

Publication Verification of Combinational Logic in Nuprl | cite »
by David A. Basin, Peter Del Vecchio
1989

Publication An Environment for Automated Reasoning About Partial Functions | cite »
by David A. Basin
1988

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
April 08, 1988

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
October 13, 1987

Seminar The Expressiveness of lambda Y
by David A. Basin
April 09, 1987

Bates, Joseph L.

Publication Proofs as Programs | cite »
by Joseph L. Bates, Robert L. Constable
1985

Publication Writing Programs That Construct Proofs | cite »
by Robert L. Constable, Todd B. Knoblock, Joseph L. Bates
1984

Publication A Logic for Correct Program Development | cite »
by Joseph L. Bates
1981

Beck, John

Seminar Category Theory as Basis for Mathematics
by John Beck
December 02, 1986

Benzinger, Ralph

Publication Automated Complexity Analysis of Nuprl Extracted Programs | cite »
by Ralph Benzinger
2001

Publication Automated Computational Complexity Analysis | cite »
by Ralph Benzinger
2001

Seminar Automated Higher-Order Complexity Analysis
by Ralph Benzinger
February 05, 2001

Seminar Automatic Complexity Analysis Revisited
by Ralph Benzinger
January 31, 2000

Seminar Automated Complexity Analysis
by Ralph Benzinger
September 15, 1998

Berger, Ulrich

Publication Logic, Construction, Computation | cite »
by Ulrich Berger
July 29, 2012

Bertot, Yves

Seminar Mechanizing the Proof of Correction of a Compiler Using Type Theory
by Yves Bertot
November 17, 1998

Bickford, Mark

Publication Cubical type theory with several universes in Nuprl
by Mark Bickford
May 20, 2020

Publication Formalization of Cubical Type Theory in Nuprl
by Mark Bickford
January 15, 2020

Publication DRAFT: Brouwer's Fixedpoint Theorem in Intuitionistic Mathematics
by Mark Bickford
February 18, 2020

Publication Open Bar -- A Reconciliation between Intuitionistic and Classical Logic
by Vincent Rahli, Mark Bickford, Robert L. Constable, Liron Cohen
2020

Math Book An Intuitionistic Formalization of The Elements of Euclid Book I
by Ariel Kellison, Mark Bickford
November 26, 2019

Publication Bar Induction is Compatible with Constructive Type Theory | cite »
by Vincent Rahli, Liron Cohen, Mark Bickford, Robert L. Constable
2019

Publication Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl | cite »
by Mark Bickford
2018

Publication Validating Brouwerâ€™s Continuity Principle for Numbers Using Named Exceptions | cite »
by Vincent Rahli, Mark Bickford
January 02, 2018

Publication Connectedness of the Continuum in Intuitionistic Mathematics | cite »
by Mark Bickford
2018

Publication Computability Beyond Church-Turing using Choice Sequences | cite »
by Liron Cohen, Vincent Rahli, Mark Bickford, Robert L. Constable
2018

Publication Implementing Euclid's Straightedge and Compass Constructions in Type Theory | cite »
by Ariel Kellison, Mark Bickford, Robert L. Constable
2018

Publication A Verified Theorem Prover Backend Supported by a Monotonic Library | cite »
by Vincent Rahli, Liron Cohen, Mark Bickford
November 01, 2018

Publication Bar Induction: The Good, the Bad, and the Ugly | cite »
by Vincent Rahli, Mark Bickford, Robert L. Constable
April 11, 2017

Publication 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

Publication Constructive Analysis and Experimental Mathematics using the Nuprl Proof Assistant
by Mark Bickford
March 02, 2016

Publication A Nominal Exploration of Intuitionism
by Vincent Rahli, Mark Bickford
January 18, 2016

Publication Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
September 01, 2015

Publication Coq as a Metatheory for Nuprl with Bar Induction
by Vincent Rahli, Mark Bickford
September 14, 2015

Publication Nuprlâ€™s Inductive Logical Forms
by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli
September 01, 2015

Publication Intuitionistic Completeness of First-Order Logic | cite »
by Robert L. Constable, Mark Bickford
January 01, 2014

Publication Inductive Construction in Nuprl Type Theory Using Bar Induction
by Mark Bickford, Robert L. Constable
May 12, 2014

Math Book A Fast Algorithm for the Integer Square Root
by Anne Trostle, Mark Bickford
June 09, 2014

Seminar Synthesizing Protocols using the Logic of Events and EventML
by Robert L. Constable, Mark Bickford
September 17, 2014

Seminar Topics in Type Theory
by Abhishek Anand, Robert L. Constable, Mark Bickford
October 22, 2014

Seminar Nominal Type Theory
by Mark Bickford, Vincent Rahli
October 29, 2014

Seminar From Replicated Databases to Ensembles of Collaborating Robots
by Abhishek Anand, Mark Bickford
November 19, 2014

Publication Developing Correctly Replicated Databases Using Formal Tools
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
June 23, 2014

Publication A Type Theory with Partial Equivalence Relations as Types
by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli
May 12, 2014

Seminar Formalizing Bishop's Constructive Analysis in Constructive Type Theory
by Mark Bickford, Robert L. Constable
April 10, 2014

Seminar There Are No Discontinuous Real Functions
by Mark Bickford, Vincent Rahli
October 08, 2014

Seminar Synthetic Topology in NuPRL
by Francisco Mota, Mark Bickford
December 03, 2014

Publication Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types | cite »
by Vincent Rahli, Mark Bickford, Abhishek Anand
April 22, 2013

Publication Formal Specification, Verification, and Implementation of Fault-Tolerant Systems
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
March 31, 2013

Seminar The power of bar induction in constructive type theory
by Mark Bickford
September 25, 2013

Seminar Quotient Types in Nuprl
by Mark Bickford
November 13, 2013

Publication The Logic of Events, a framework to reason about distributed systems | cite »
by Mark Bickford, Vincent Rahli, Robert L. Constable
2012

Math Book Introduction to EventML
by Mark Bickford, Robert L. Constable, Richard Eaton, David Guaspari
February 03, 2012

Math Book Formalizing Moessner's Theorem in Nuprl
by Mark Bickford, Dexter Kozen, Alexandra Silva
June 08, 2012

Math Book Formalizing Constructive Analysis in Nuprl
by Mark Bickford
September 04, 2012

Seminar Wider Deployment of Nuprl
by Richard Eaton, Mark Bickford, Robert L. Constable, Christoph Kreitz
September 28, 2012

Seminar Bar Induction and the Fan Theorem in Constructive Type Theory
by Robert L. Constable, Mark Bickford, Abhishek Anand
October 12, 2012

Publication 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

Publication Polymorphic Logic | cite »
by Mark Bickford, Robert L. Constable
July 29, 2012

Publication 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

Seminar Realizing Bar Induction in Nuprl
by Mark Bickford
October 26, 2012

Seminar NuPRL Demo
by Mark Bickford
September 16, 2011

Seminar Simple Consensus Algorithm
by Robert L. Constable, Mark Bickford, Vincent Rahli
October 28, 2011

Seminar Impredicative vs Predicative Type Theory
by Robert L. Constable, Mark Bickford, Richard Eaton
April 13, 2012

Seminar Adding Communication Primitives to the Nuprl Evaluator
by Mark Bickford
May 04, 2012

Publication Intuitionistic Completeness of First-Order Logic | cite »
by Robert L. Constable, Mark Bickford
October 07, 2011

Publication Generating Event Logics with Higher-Order Processes as Realizers | cite »
by Mark Bickford, Robert L. Constable, David Guaspari
2010

Publication Automated Proof of Authentication Protocols in a Logic of Events | cite »
by Mark Bickford
2010

Publication Investigating Correct-by-Construction Attack-Tolerant Systems | cite »
by Robert L. Constable, Mark Bickford, Robbert van Renesse
2010

Publication Component Specification Using Event Classes | cite »
by Mark Bickford
2009

Publication Formal Foundations of Computer Security | cite »
by Mark Bickford, Robert L. Constable
2008

Publication Unguessable Atoms: A Logical Foundation for Security | cite »
by Mark Bickford
2008

Publication 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

Math Book Chain Replication Protocol
by Mark Bickford
September 27, 2006

Publication Formalizing chain replication
by Mark Bickford, David Guaspari
2006

Publication Unguessable Atoms: A Logical Foundation for Security | cite »
by Mark Bickford
2006

Seminar Automating Proofs in Event Logic
by Mark Bickford, Richard Eaton
August 26, 2005

Seminar Automated Proofs in Event Logic
by Mark Bickford
September 16, 2005

Seminar Urelements in Type Theory: New Definition of "Inherence"
by Mark Bickford
November 18, 2005

Seminar Automating Proofs in Event Logic
by Mark Bickford, Richard Eaton
March 23, 2006

Seminar Event Systems: Introduction to the Logic of Events
by Mark Bickford
February 17, 2006

Publication A Causal Logic of Events in Formalized Computational Type Theory | cite »
by Mark Bickford, Robert L. Constable
2005

Publication Knowledge-based synthesis of distributed systems using event structures | cite »
by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2005

Publication A Programming Logic for Distributed Systems | cite »
by Mark Bickford, David Guaspari
2005

Seminar Real-time Message Automata
by Mark Bickford
February 11, 2005

Seminar Mark Presentation
by Mark Bickford
November 29, 2004

Seminar Urelements in Computational Type Theory
by Mark Bickford
November 11, 2005

Publication Knowledge-Based Synthesis of Distributed Systems Using Event Structures
by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2004

Seminar The Logic of Events and Event Structure Patterns
by Mark Bickford
April 26, 2004

Seminar Leader Election Protocols
by Mark Bickford
October 06, 2003

Publication A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics | cite »
by Jon Kleinberg, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz
2003

Math Book Event Systems
by Mark Bickford
November 08, 2003

Math Book Graph Theory
by Mark Bickford
May 14, 2003

Math Book General Automata Theory
by Mark Bickford
January 25, 2003

Publication A Logic of Events | cite »
by Mark Bickford, Robert L. Constable
2003

Seminar Implementing the Logic of Events
by Mark Bickford
February 24, 2003

Seminar Application of Event Systems and the Logic of Distributed Systems to Leader Election
by Mark Bickford
September 30, 2002

Seminar Introduction to Event Systems and the Logic of Distributed Systems
by Mark Bickford, Robert L. Constable
September 16, 2002

Math Book Hybrid Protocols
by Mark Bickford
February 20, 2002

Publication FDL: A Prototype Formal Digital Library
by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2002

Seminar Recent Results on the PCES Project
by Mark Bickford
April 01, 2002

Seminar Report on the DARPA PCES PI meeting
by Robert L. Constable, Lori Lorigo, Mark Bickford
October 29, 2001

Seminar Processing video streams using event notification systems
by Robert L. Constable, Mark Bickford
October 15, 2001

Seminar More on proof automation: Shostak's decision procedure and Nuprl
by Mark Bickford
September 24, 2001

Publication An Experiment in Formal Design Using Meta-Properties | cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Robert L. Constable
2001

Publication Proving Hybrid Protocols Correct | cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu
2001

Publication Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment | cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse
2001

Publication Protocol Switching: Exploiting Meta-Properties | cite »
by Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable
2001

Seminar Continuation on reflection
by Mark Bickford
March 13, 2000

Seminar IO-automata and Ensemble
by Mark Bickford
February 21, 2000

Publication An Object-Oriented Approach to Verifying Group Communication Systems | cite »
by Mark Bickford, Jason Hickey
1999

Birman, Kenneth

Publication 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

Publication 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

Bridges, Douglas

Seminar Computational Content of Math
by Douglas Bridges
October 19, 1993

Bromley, H. M.

Seminar ML Execution
by H. M. Bromley
1984-1985

Seminar Nuprl Execution
by H. M. Bromley
1984-1985

Brown, Geoffrey

Publication Formally Verified Synthesis of Combinational Circuits | cite »
by David A. Basin, Geoffrey Brown, Miriam Leeser
1991

Bryukhov, Yegor

Seminar Arithmetic module for MetaPRL: rules and Arith tactic
by Yegor Bryukhov
March 25, 2002

Bundy, Alan

Publication The Oyster-Clam System | cite »
by Alan Bundy, Frank Van Harmelen, Christian Horn, Alan Smaill
1990

Caldwell, James L.

Math Book Classical Propositional Logic
by James L. Caldwell
July 28, 2004

Publication Logical Aspects of Digital Mathematics Libraries (extended abstract) | cite »
by Stuart F. Allen, James L. Caldwell, Robert L. Constable
2001

Publication Search Algorithms in Type Theory | cite »
by James L. Caldwell, Ian Gent, Judith Underwood
2000

Publication Intuitionistic Tableau Extracted | cite »
by James L. Caldwell
1999

Publication Classical Propositional Decidability via Nuprl Proof Extraction | cite »
by James L. Caldwell
1998

Publication Decidability Extracted: Synthesizing | cite »
by James L. Caldwell
1998

Seminar Extracting Readable and Efficient Programs from Nuprl Proofs
by James L. Caldwell
November 18, 1997

Publication Extracting Propositional Decidability: A Proof of Propositional Decidability in Constructive Type Theory and its Extracted Program | cite »
by James L. Caldwell
1997

Publication Moving Proofs-as-Programs into Practice | cite »
by James L. Caldwell
1997

Publication Classical Tools for Constructive Proof Search | cite »
by James L. Caldwell, Judith Underwood
1996

Seminar Formal Methods Program at NASA Langley Research Center
by James L. Caldwell
February 07, 1995

Chan, Tat-hung

Publication Reversal-Bounded Computations | cite »
by Tat-hung Chan
1980

Chen, Wilfred Z.

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
May 04, 1993

Publication Tactic-Based Theorem Proving and Knowledge-Based Forward Chaining: An Experiment with Nuprl and Ontic | cite »
by Wilfred Z. Chen
1992

Seminar How to Strengthen the Notion of Obvious Step
by Wilfred Z. Chen
October 22, 1991

Seminar CADE Practice Talk
by Wilfred Z. Chen
May 12, 1992

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
April 08, 1988

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
October 13, 1987

Cheney, James

Seminar Randomized Programming and Probabilistic Reasoning in Type Theory
by James Cheney
April 17, 2000

Cheung, Crystal

Publication Brouwer's Fan Theorem: An Overview
by Crystal Cheung
2015

Chew, Paul

Publication Collaborative Mathematics Environments | cite »
by Robert L. Constable, Paul Chew, Keshav Pingali, Steve Vavasis, Richard Zippel
1996

Cleaveland, Walter Rance

Publication Type-Theoretic Models of Concurrency | cite »
by Walter Rance Cleaveland
1987

Seminar Implementing Finite Sets
by Walter Rance Cleaveland
September 09, 1986

Cohen, Liron

Publication Open Bar -- A Reconciliation between Intuitionistic and Classical Logic
by Vincent Rahli, Mark Bickford, Robert L. Constable, Liron Cohen
2020

Publication Bar Induction is Compatible with Constructive Type Theory | cite »
by Vincent Rahli, Liron Cohen, Mark Bickford, Robert L. Constable
2019

Publication Automated Reasoning in Herbrand Structures
by Liron Cohen, Reuben Rowe, Yoni Zohar
June 03, 2019

Publication Computability Beyond Church-Turing using Choice Sequences | cite »
by Liron Cohen, Vincent Rahli, Mark Bickford, Robert L. Constable
2018

Publication A Verified Theorem Prover Backend Supported by a Monotonic Library | cite »
by Vincent Rahli, Liron Cohen, Mark Bickford
November 01, 2018

Publication Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent | cite »
by Liron Cohen, Reuben Rowe
July 01, 2018

Publication Intuitionistic Ancestral Logic
by Liron Cohen, Robert L. Constable
October 10, 2015

Seminar Intuitionistic Ancestral Logic
by Liron Cohen
July 12, 2012

Constable, Robert L.

Publication Computer Science at the Frontiers of Mathematics
by Robert L. Constable
January 15, 2020

Publication The Continuum
by Robert L. Constable
February 26, 2020

Publication Open Bar -- A Reconciliation between Intuitionistic and Classical Logic
by Vincent Rahli, Mark Bickford, Robert L. Constable, Liron Cohen
2020

Publication Bar Induction is Compatible with Constructive Type Theory | cite »
by Vincent Rahli, Liron Cohen, Mark Bickford, Robert L. Constable
2019

Publication Computability Beyond Church-Turing using Choice Sequences | cite »
by Liron Cohen, Vincent Rahli, Mark Bickford, Robert L. Constable
2018

Publication Implementing Euclid's Straightedge and Compass Constructions in Type Theory | cite »
by Ariel Kellison, Mark Bickford, Robert L. Constable
2018

Publication Bar Induction: The Good, the Bad, and the Ugly | cite »
by Vincent Rahli, Mark Bickford, Robert L. Constable
April 11, 2017

Math Book A Formal Exploration of Constructive Geometry
by Sarah Sernaker, Robert L. Constable
2016

Publication A Formal Exploration of Constructive Geometry
by Robert L. Constable, Sarah Sernaker
2016

Math Book Constructive Reading of Classical Logic
by Robert L. Constable, Sarah Sernaker
2015

Publication Intuitionistic Ancestral Logic
by Liron Cohen, Robert L. Constable
October 10, 2015

Publication Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
September 01, 2015

Publication Nuprlâ€™s Inductive Logical Forms
by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli
September 01, 2015

Publication Intuitionistic Completeness of First-Order Logic | cite »
by Robert L. Constable, Mark Bickford
January 01, 2014

Publication Inductive Construction in Nuprl Type Theory Using Bar Induction
by Mark Bickford, Robert L. Constable
May 12, 2014

Math Book Logical Investigations, with the Nuprl Proof Assistant
by Robert L. Constable, Anne Trostle
July 22, 2014

Seminar Synthesizing Protocols using the Logic of Events and EventML
by Robert L. Constable, Mark Bickford
September 17, 2014

Seminar Topics in Type Theory
by Abhishek Anand, Robert L. Constable, Mark Bickford
October 22, 2014

Publication Developing Correctly Replicated Databases Using Formal Tools
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
June 23, 2014

Publication A Type Theory with Partial Equivalence Relations as Types
by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli
May 12, 2014

Seminar Formalizing Bishop's Constructive Analysis in Constructive Type Theory
by Mark Bickford, Robert L. Constable
April 10, 2014

Publication Virtual Evidence: A Constructive Semantics for Classical Logics
by Robert L. Constable
2014

Publication The Logic of Information Flow and the Foundations of Distributed Computing
by Robert L. Constable
January 10, 2013

Seminar Nuprl as a Programming Assistant
by Robert L. Constable
November 06, 2013

Publication Formal Specification, Verification, and Implementation of Fault-Tolerant Systems
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
March 31, 2013

Seminar An Extension of OCaml's Type Theory
by Robert L. Constable
October 23, 2013

Math Book Introduction to EventML
by Mark Bickford, Robert L. Constable, Richard Eaton, David Guaspari
February 03, 2012

Publication Proof Assistants and the Rise of Type Theory Circa 1912-2012
by Robert L. Constable
March 19, 2012

Publication Type Theoretic Semantics for First-Order Logic
by Robert L. Constable
May 24, 2012

Publication Proof Assistants and the Dynamic Nature of Formal Theories | cite »
by Robert L. Constable
June 29, 2012

Publication Proofs as Process
by Robert L. Constable
2012

Seminar Wider Deployment of Nuprl
by Richard Eaton, Mark Bickford, Robert L. Constable, Christoph Kreitz
September 28, 2012

Seminar Bar Induction and the Fan Theorem in Constructive Type Theory
by Robert L. Constable, Mark Bickford, Abhishek Anand
October 12, 2012

Publication 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

Publication Next Generation Proof Technology
by Robert L. Constable
December 27, 2012

Publication The Logic of Events, a framework to reason about distributed systems | cite »
by Mark Bickford, Vincent Rahli, Robert L. Constable
2012

Publication On Building Constructive Formal Theories of Computation Noting the Roles of Turing, Church, and Brouwer | cite »
by Robert L. Constable
June 29, 2012

Seminar Introduction to the Fall Seminar Series
by Robert L. Constable
September 07, 2012

Publication Polymorphic Logic | cite »
by Mark Bickford, Robert L. Constable
July 29, 2012

Publication Russell's Orders in Kripke's Theory of Truth and Computational Type Theory | cite »
by Robert L. Constable, Fairouz Kamareddine, Twan Laan
2012

Publication 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

Seminar Seminar History and Initial Planning Meeting
by Robert L. Constable
September 09, 2011

Seminar Seminar History and Initial Planning Meeting
by Robert L. Constable, Robert L. Constable
September 09, 2011

Seminar Analyzing Access Control Logics Using Evidence Semantics
by Robert L. Constable
September 23, 2011

Seminar Simple Consensus Algorithm
by Robert L. Constable, Mark Bickford, Vincent Rahli
October 28, 2011

Seminar Stronger Role for Recursive Types Needed for Logic of Events
by Robert L. Constable
February 24, 2012

Seminar Reviewing Nuprl
by Robert L. Constable
March 09, 2012

Seminar Impredicative vs Predicative Type Theory
by Robert L. Constable, Mark Bickford, Richard Eaton
April 13, 2012

Publication Intuitionistic Completeness of First-Order Logic | cite »
by Robert L. Constable, Mark Bickford
October 07, 2011

Publication Generating Event Logics with Higher-Order Processes as Realizers | cite »
by Mark Bickford, Robert L. Constable, David Guaspari
2010

Publication Investigating Correct-by-Construction Attack-Tolerant Systems | cite »
by Robert L. Constable, Mark Bickford, Robbert van Renesse
2010

Publication The Triumph of Types: Principia Mathematica's Impact on Computer Science | cite »
by Robert L. Constable
2010

Publication Building Mathematics-Based Software Systems to Advance Science and Create Knowledge | cite »
by Robert L. Constable
2009

Publication Formal Foundations of Computer Security | cite »
by Mark Bickford, Robert L. Constable
2008

Publication Effectively Nonblocking Consensus Procedures Can Execute Forever - a Constructive Version of FLP | cite »
by Robert L. Constable
2008

Publication Computational Type Theory -- Extended Version | cite »
by Robert L. Constable
2008

Publication Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus | cite »
by Wojciech Moczydlowski, Robert L. Constable
2007

Publication Transforming the Academy: Knowledge Formation in the Age of Digital Information
by Robert L. Constable
January 11, 2007

Publication 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

Publication Enabling Large Scale Coherency Among Mathematical Texts | cite »
by Stuart F. Allen, Robert L. Constable
2006

Publication Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts | cite »
by Stuart F. Allen, Robert L. Constable, Lori Lorigo
2006

Publication Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics | cite »
by Robert L. Constable, Wojciech Moczydlowski
2006

Publication Information-Intensive Proof Technology | cite »
by Robert L. Constable
2006

Publication A Causal Logic of Events in Formalized Computational Type Theory | cite »
by Mark Bickford, Robert L. Constable
2005

Publication Knowledge-based synthesis of distributed systems using event structures | cite »
by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2005

Seminar Randomness and Free Choice Sequences
by Robert L. Constable
February 04, 2005

Seminar Remarks on Nijmegen trip
by Robert L. Constable
November 08, 2004

Seminar Foundations for the Management of Formal Mathematical Knowledge
by Robert L. Constable
October 25, 2004

Seminar Automated Reasoning in Category Theory
by Robert L. Constable
October 04, 2004

Publication 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

Publication Knowledge-Based Synthesis of Distributed Systems Using Event Structures
by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2004

Publication 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

Seminar Important Episodes in the History of Constructive Mathematics--including the frog and mouse wars
by Robert L. Constable
March 01, 2004

Seminar Comparing Aspects of Set Theory and Type Theory
by Robert L. Constable
February 16, 2004

Seminar Planning Session for Spring Seminar Series
by Robert L. Constable
January 26, 2004

Seminar Steps Toward a World Wide Digital Library of Formal Algorithmic Knowledge
by Robert L. Constable
October 27, 2003

Seminar An Introduction to Event Systems
by Robert L. Constable
September 29, 2003

Seminar Introduction to the Fall Seminar Series
by Robert L. Constable
September 08, 2003

Publication A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics | cite »
by Jon Kleinberg, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz
2003

Publication Practical Reflection in Nuprl | cite »
by Eli Barzilay, Stuart F. Allen, Robert L. Constable
2003

Publication A Logic of Events | cite »
by Mark Bickford, Robert L. Constable
2003

Publication Recent Results in Type Theory and Their Relationship to Automath | cite »
by Robert L. Constable
2003

Publication MetaPRL -- A Modular Logical Environment | cite »
by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo
2003

Seminar Continuing Discussion of the NSDL
by Robert L. Constable
April 14, 2003

Seminar Enabling Active Mathematical Documents in the National Science Digital Library
by Robert L. Constable
March 31, 2003

Seminar Uri Abraham's Models for Concurrency
by Robert L. Constable, Sabina Petride
January 27, 2003

Seminar Continuing Discussion of Objects
by Alexei Kopylov, Robert L. Constable
December 02, 2002

Seminar Classes and Objects
by Robert L. Constable
November 25, 2002

Seminar Introduction to Event Systems and the Logic of Distributed Systems
by Mark Bickford, Robert L. Constable
September 16, 2002

Publication Computational Complexity and Induction for Partial Computable Functions in Type Theory | cite »
by Robert L. Constable, Karl Crary
2002

Publication Naive Computational Type Theory | cite »
by Robert L. Constable
2002

Publication FDL: A Prototype Formal Digital Library
by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2002

Seminar Properties of the Formal Digital Library
by Robert L. Constable
May 06, 2002

Seminar Report on the Edinburgh Conference: 35 Years of Automath
by Robert L. Constable
2001-2002

Seminar Report on the Design of the Formal Digital Library
by Richard Eaton, Robert L. Constable, Stuart F. Allen
April 08, 2002

Seminar Explaining the Formal Digital Library
by Stuart F. Allen, Robert L. Constable, Richard Eaton
March 11, 2002

Seminar Embedded Ststems
by Christoph Kreitz, Robert L. Constable
November 05, 2001

Seminar Report on the DARPA PCES PI meeting
by Robert L. Constable, Lori Lorigo, Mark Bickford
October 29, 2001

Seminar Progress on the ONR University Research Initiative in Digital Libraries for Computational Mathematics
by Stuart F. Allen, Robert L. Constable
December 03, 2001

Seminar Processing video streams using event notification systems
by Robert L. Constable, Mark Bickford
October 15, 2001

Publication Logical Aspects of Digital Mathematics Libraries (extended abstract) | cite »
by Stuart F. Allen, James L. Caldwell, Robert L. Constable
2001

Math Book Finite Automata
by Robert L. Constable
May 16, 2001

Publication An Experiment in Formal Design Using Meta-Properties | cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Robert L. Constable
2001

Publication Protocol Switching: Exploiting Meta-Properties | cite »
by Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable
2001

Seminar NSF ITR proposal
by Robert L. Constable, Robert L. Constable
March 26, 2001

Seminar NSF ITR proposal
by Robert L. Constable, Robert L. Constable
March 12, 2001

Seminar How Nuprl Reasons
by Robert L. Constable
January 29, 2001

Seminar Research Directions
by Robert L. Constable
September 25, 2000

Seminar Reading BAAs and RFPs
by Robert L. Constable
October 16, 2000

Seminar Reading BAAs and RFPs (cont.)
by Robert L. Constable
October 23, 2000

Seminar Discussing the issues surrounding our library of formal algorithmic mathematics
by Robert L. Constable
November 13, 2000

Publication The Nuprl Open Logical Environment | cite »
by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2000

Publication Nuprl's Class Theory and Its Applications | cite »
by Robert L. Constable, Jason Hickey
2000

Seminar Intersections, Unions and Games
by Robert L. Constable, Alexei Kopylov, Aleksey Nogin
December 06, 1999

Seminar Points of Contact with Girard (Nuprl ∩ Ludics)
by Robert L. Constable
September 13, 1999

Publication Verbalization of High-Level Formal Proofs | cite »
by Amanda Holland-Minkley, Regina Barzilay, Robert L. Constable
1999

Publication Metalogical Frameworks II: Developing a Reflected Decision Procedure | cite »
by William Aitken, Robert L. Constable, Judith Underwood
1999

Seminar Semantics and Pragmatics of Reflected Proof
by Stuart F. Allen, Sergei Artemov, Robert L. Constable
December 01, 1998

Seminar Listening to Theorem Provers who Talk to Each Other about Computer Systems
by Robert L. Constable
October 20, 1998

Seminar Some Uses of the Intersection Type
by Stuart F. Allen, Robert L. Constable
May 03, 1999

Seminar Reflection Mechanisms in Nuprl
by Stuart F. Allen, Robert L. Constable
November 10, 1998

Seminar On Modeling Ensemble
by Robert L. Constable, Jason Hickey
October 27, 1998

Publication The Structure of Nuprl's Type Theory | cite »
by Robert L. Constable
1997

Seminar Computability is Ineffable in ZF Set Theory
by Robert L. Constable
April 01, 1997

Seminar Discussion of Issues in Logic Library Design
by Robert L. Constable, Jason Hickey, Stuart F. Allen, Richard Eaton
March 03, 1997

Publication Collaborative Mathematics Environments | cite »
by Robert L. Constable, Paul Chew, Keshav Pingali, Steve Vavasis, Richard Zippel
1996

Math Book Collaborative Mathematics Environments
by Robert L. Constable
November 21, 1996

Publication Formalizing Automata Theory I: Finite Automata | cite »
by Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe
1996

Publication Formalizing Automata II: Decidable Properties | cite »
by Robert L. Constable, Pavel Naumov
1996

Publication The Value of Automated Deduction | cite »
by Robert L. Constable
1996

Publication Creating and Evaluating Interactive Formal Courseware for Mathematics and Computing | cite »
by Robert L. Constable
1996

Seminar Project Direction and Research Problems
by Robert L. Constable
February 06, 1996

Publication Expressing Computational Complexity in Constructive Type Theory | cite »
by Robert L. Constable
1995

Publication Experience Using Type Theory as a Foundation for Computer Science Circa 1985-1995 | cite »
by Robert L. Constable
1995

Seminar Defining the Polynomial Time Functions over N in Nuprl
by Robert L. Constable
March 28, 1995

Seminar An Open Architecture for Nuprl
by Robert L. Constable
March 01, 1995

Seminar Representing Computational Complexity in Nuprl
by Robert L. Constable
November 22, 1994

Publication Exporting and Reflecting Abstract Meta-mathematics | cite »
by Robert L. Constable
1994

Publication Towards Integrated Systems for Symbolic Algebra and Formal Constructive Mathematics | cite »
by Robert L. Constable, Paul B. Jackson
1994

Publication Using Reflection to Explain and Enhance Type Theory | cite »
by Robert L. Constable
1994

Seminar Theorem Proving with Real Numbers
by Robert L. Constable
August 31, 1993

Seminar Project Overview
by Robert L. Constable
July 01, 1993

Seminar Predicative Higher-Order PROPOSITIONAL Logic vs. the Impredicative Propositional Calculus
by Robert L. Constable, Robert L. Constable
April 19, 1993

Publication Lectures on: Classical Proofs as Programs | cite »
by Robert L. Constable
1992

Publication Metalevel Programming in Constructive Type Theory | cite »
by Robert L. Constable
1992

Publication Formal Theories and Software Systems: Fundamental Connections Between Computer Science and Logic | cite »
by Robert L. Constable
1992

Publication Finding Computational Content from Classical Proofs | cite »
by Robert L. Constable, Chetan Murthy
1991

Publication Type Theory as a Foundation for Computer Science | cite »
by Robert L. Constable
1991

Publication Metalogical Frameworks | cite »
by David A. Basin, Robert L. Constable
1991

Publication The Semantics of Reflected Proof | cite »
by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken
1990

Publication Reflecting the Open-Ended Computation System of Constructive Type Theory | cite »
by Robert L. Constable, Stuart F. Allen, Douglas J. Howe
1990

Publication Nuprl as a General Logic | cite »
by Robert L. Constable, Douglas J. Howe
1990

Publication Implementing Metamathematics as an Approach to Automatic Theorem Proving | cite »
by Robert L. Constable, Douglas J. Howe
1990

Publication Assigning Meaning to Proofs: A Semantic Basis for Problem Solving Environments | cite »
by Robert L. Constable
1989

Seminar Collaborative Problem Solving Environment
by Robert L. Constable
1988

Publication Computational Foundations of Basic Recursive Function Theory | cite »
by Robert L. Constable, Scott F. Smith
1988

Seminar Typed Enumeration-Free External Setting for Computing Theory
by Robert L. Constable
November 03, 1987

Publication Partial Objects in Constructive Type Theory | cite »
by Scott F. Smith, Robert L. Constable
1987

Publication Formalized Metareasoning in Type Theory | cite »
by Todd B. Knoblock, Robert L. Constable
1986

Publication Infinite Objects in Type Theory | cite »
by Nax P. Mendler, Robert L. Constable, Prakash Panangaden
1986

Publication Proofs as Programs | cite »
by Joseph L. Bates, Robert L. Constable
1985

Publication Recursive Definitions in Type Theory | cite »
by Robert L. Constable, Nax P. Mendler
1985

Publication Constructive Mathematics as a Programming Logic I: Some Principles of Theory | cite »
by Robert L. Constable
1985

Publication Semantics of Evidence | cite »
by Robert L. Constable
1985

Seminar Universally Closed Classes
by Robert L. Constable
1984-1985

Publication Writing Programs That Construct Proofs | cite »
by Robert L. Constable, Todd B. Knoblock, Joseph L. Bates
1984

Publication A Hierarchical Approach to Formal Semantics With Application to the Definition of PL/ CS | cite »
by Robert L. Constable, James Donahue
July 01, 1979

Publication A Programming Logic | cite »
by Robert L. Constable, Michael J. O'Donnell
1978

Publication A Constructive Programming Logic
by Robert L. Constable
August 08, 1977

Publication Constructive Mathematics and Automatic Program Writers | cite »
by Robert L. Constable
1971

Crary, Karl

Math Book Bar-Type Rules
by Karl Crary
January 25, 2002

Publication Computational Complexity and Induction for Partial Computable Functions in Type Theory | cite »
by Robert L. Constable, Karl Crary
2002

Publication Type-Theoretic Methodology for Practical Programming Languages | cite »
by Karl Crary
1998

Seminar Simple, Efficient Object Encoding using Intersection Types
by Karl Crary
April 14, 1998

Seminar Type Methodology for Modern Languages and Compilers
by Karl Crary
February 24, 1998

Seminar From System F to Typed Assembly Language
by Karl Crary
September 16, 1997

Publication Foundations for the Implementation of Higher-Order Subtyping | cite »
by Karl Crary
1997

Seminar Formal Continuations and Classical Logic
by Karl Crary
March 10, 1997

Seminar Advancing the Type-Theoretic Underpinnings of Practical Programming Languages
by Karl Crary
1996-1997

Seminar Foundations for the Implementation of Higher-Order Subtyping: Part II
by Karl Crary
November 12, 1996

Seminar Foundations for the Implementation of Higher-Order Subtyping
by Karl Crary
November 05, 1996

Seminar KML
by Karl Crary
April 30, 1996

Cremer, J. F.

deBruijn, N. G.

Seminar Math Vernacular
by N. G. deBruijn
November 17, 1987

Del Vecchio, Peter

Publication Verification of Combinational Logic in Nuprl | cite »
by David A. Basin, Peter Del Vecchio
1989

Donahue, James

Publication 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

Publication Nuprlâ€™s Inductive Logical Forms
by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli
September 01, 2015

Math Book Introduction to EventML
by Mark Bickford, Robert L. Constable, Richard Eaton, David Guaspari
February 03, 2012

Math Book Work in Progress
by Richard Eaton
February 20, 2012

Seminar Wider Deployment of Nuprl
by Richard Eaton, Mark Bickford, Robert L. Constable, Christoph Kreitz
September 28, 2012

Seminar Impredicative vs Predicative Type Theory
by Robert L. Constable, Mark Bickford, Richard Eaton
April 13, 2012

Publication 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

Math Book Automatic FDL Projections
by Richard Eaton
September 01, 2006

Seminar Automating Proofs in Event Logic
by Mark Bickford, Richard Eaton
August 26, 2005

Seminar Automating Proofs in Event Logic
by Mark Bickford, Richard Eaton
March 23, 2006

Publication A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics | cite »
by Jon Kleinberg, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz
2003

Publication FDL: A Prototype Formal Digital Library
by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2002

Seminar Report on the Design of the Formal Digital Library
by Richard Eaton, Robert L. Constable, Stuart F. Allen
April 08, 2002

Seminar Explaining the Formal Digital Library
by Stuart F. Allen, Robert L. Constable, Richard Eaton
March 11, 2002

Publication The Nuprl Open Logical Environment | cite »
by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2000

Seminar The Nuprl 5 Library
by Richard Eaton
February 09, 1998

Seminar Discussion of Issues in Logic Library Design
by Robert L. Constable, Jason Hickey, Stuart F. Allen, Richard Eaton
March 03, 1997

Seminar Design and Implemention of the Library Component of Nuprl 5
by Richard Eaton
October 03, 1995

Seminar The "Interface" Version of Nuprl
by Stuart F. Allen, Richard Eaton
November 15, 1994

Egly, Uwe

Seminar On Intuitionistic Proof Transformations and their Application to Constructive Program Synthesis
by Uwe Egly
September 22, 1998

Evfimievski, Sasha

Fluet, Matthew

Publication 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

Seminar Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations
by Matthew Fluet
November 24, 2003

Seminar Variations on a Proof by Smullyan
by Matthew Fluet
May 05, 2003

Seminar The Calculemus Autumn School
by Christoph Kreitz, Sabina Petride, Matthew Fluet
October 28, 2002

Forester, Max B.

Publication Formalizing Constructive Real Analysis | cite »
by Max B. Forester
1993

Gent, Ian

Publication Search Algorithms in Type Theory | cite »
by James L. Caldwell, Ian Gent, Judith Underwood
2000

Seminar The Enigma of Sat Hill Climbing Procedures
by Ian Gent
November 10, 1992

Geser, Alfons

Publication Termination of Single-Threaded One-rule Semi-Thue Systems | cite »
by Wojciech Moczydlowski, Alfons Geser
2005

Giunchiglia, Fausto

Publication Reflection in Constructive and Non-Constructive Automated Reasoning | cite »
by Fausto Giunchiglia, Alan Smaill
1989

Glew, Neal

Seminar Typed Assembly Language
by Neal Glew
March 01, 1999

Seminar Formal Domain Theory
by Neal Glew
December 05, 1995

Gonthier, Georges

Seminar Verifying the Four Colour Theorem
by Georges Gonthier
May 20, 2005

Griffin, Timothy G.

Publication Notational Definition and Top-down Refinement for Interactive Proof Development Systems | cite »
by Timothy G. Griffin
1988

Seminar Syntactic Abstraction
by Timothy G. Griffin
September 22, 1987

Seminar Using Lemmas
by Timothy G. Griffin
1984-1985

Seminar Arithpac
by Timothy G. Griffin
1984-1985

Guaspari, David

Publication Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
September 01, 2015

Publication Formal Specification, Verification, and Implementation of Fault-Tolerant Systems
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
March 31, 2013

Math Book Introduction to EventML
by Mark Bickford, Robert L. Constable, Richard Eaton, David Guaspari
February 03, 2012

Publication Encoding Pi Calculus | cite »
by David Guaspari
2010

Publication Generating Event Logics with Higher-Order Processes as Realizers | cite »
by Mark Bickford, Robert L. Constable, David Guaspari
2010

Publication Formalizing chain replication
by Mark Bickford, David Guaspari
2006

Publication A Programming Logic for Distributed Systems | cite »
by Mark Bickford, David Guaspari
2005

Hafizogullari, Ozan

Seminar Continuation of talk on Polymorphic References
by Ozan Hafizogullari
September 24, 1999

Publication Dependence Analysis Through Type Inference | cite »
by Ozan Hafizogullari, Christoph Kreitz
1999

Seminar Automatic Debugging Through Type Inference, Continued
by Ozan Hafizogullari
November 03, 1998

Seminar Automatic Debugging Through Type Inference
by Ozan Hafizogullari
October 06, 1998

Seminar Dead Code Elimination
by Ozan Hafizogullari, Christoph Kreitz
January 27, 1998

Seminar ML-like Type Reconstruction for Nuprl
by Ozan Hafizogullari
November 26, 1996

Halpern, Joseph Y.

Publication Knowledge-based synthesis of distributed systems using event structures | cite »
by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2005

Publication Knowledge-Based Synthesis of Distributed Systems Using Event Structures
by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2004

Harmelen, Frank Van

Publication The Oyster-Clam System | cite »
by Alan Bundy, Frank Van Harmelen, Christian Horn, Alan Smaill
1990

Harper, Robert W.

Seminar Lambda Calculus as Basis for Programming Language Design
by Robert W. Harper
1990-1991

Seminar The Lambda Calculus as a Basis for Language Design
by Robert W. Harper
1989-1990

Publication Aspects of the Implementation of Type Theory | cite »
by Robert W. Harper
1985

Seminar Equality
by Robert W. Harper
1984-1985

Seminar Type Inference
by Robert W. Harper
1984-1985

Hayden, Mark

Publication The Ensemble System | cite »
by Mark Hayden
1998

Publication A Proof Environment for the Development of Group Communication Systems | cite »
by Christoph Kreitz, Mark Hayden, Jason Hickey
1998

Seminar Formal Methods & Distributed Systems
by Mark Hayden
1996-1997

Seminar Group Communication with Functional Languages
by Mark Hayden
January 28, 1997

Hehner, Rick

Seminar Programs as Specification
by Rick Hehner
May 06, 1986

Hickey, Jason

Publication MetaPRL -- A Modular Logical Environment | cite »
by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo
2003

Publication Formal Compiler Implementation in a Logical Framework | cite »
by Jason Hickey, Aleksey Nogin
2003

Publication The MetaPRL Logical Programming Environment | cite »
by Jason Hickey
2001

Seminar Caltech Computer Science
by Jason Hickey
November 06, 2000

Publication Nuprl's Class Theory and Its Applications | cite »
by Robert L. Constable, Jason Hickey
2000

Publication Fast Tactic-Based Theorem Proving | cite »
by Jason Hickey, Aleksey Nogin
2000

Publication An Object-Oriented Approach to Verifying Group Communication Systems | cite »
by Mark Bickford, Jason Hickey
1999

Publication Fault-Tolerant Distributed Theorem Proving | cite »
by Jason Hickey
1999

Publication Specifications and Proofs for Ensemble Layers | cite »
by Jason Hickey, Nancy Lynch, Robbert van Renesse
1999

Seminar The Current Projects of the MetaPRL Group
by Aleksey Nogin, Jason Hickey
April 26, 1999

Seminar On Modeling Ensemble
by Robert L. Constable, Jason Hickey
October 27, 1998

Seminar A Programming Environment for Building Reliable High Performance Systems
by Jason Hickey
February 15, 1999

Publication A Proof Environment for the Development of Group Communication Systems | cite »
by Christoph Kreitz, Mark Hayden, Jason Hickey
1998

Seminar Logical Programming Environments
by Jason Hickey
March 03, 1998

Publication A Semantics of Objects in Type Theory | cite »
by Jason Hickey
1997

Publication Nuprl-Light: An Implementation Framework for Higher-Order Logics | cite »
by Jason Hickey
1997

Seminar Discussion of Issues in Logic Library Design
by Robert L. Constable, Jason Hickey, Stuart F. Allen, Richard Eaton
March 03, 1997

Seminar Modules and Libraries
by Jason Hickey
February 18, 1997

Seminar Sharing Formal Mathematics and Programming
by Jason Hickey
1996-1997

Seminar Nuprl Tutorial
by Jason Hickey
February 02, 1997

Seminar Nuprl-Light
by Jason Hickey, Jason Hickey
1996-1997

Seminar Formal Objects in Type Theory
by Jason Hickey
1996-1997

Publication Formal Objects in Type Theory Using Very Dependent Types | cite »
by Jason Hickey
1996

Seminar Formal Modules (Abstract Data Types) and Object Oriented Programming
by Jason Hickey
1995-1996

Seminar Formal Module Systems and Nuprl-Light: A Programmer's Perspective
by Jason Hickey
February 13, 1996

Seminar Verifying HORUS in Nuprl
by Jason Hickey
November 28, 1995

Seminar Formal Abstract Data Types and Inheritance
by Jason Hickey
October 31, 1995

Seminar HORUS Verification Effort
by Jason Hickey
1995-1996

Seminar Square-Root Verification
by Jason Hickey
May 10, 1995

Seminar Very Dependent Function Space
by Jason Hickey
1994-1995

Seminar The Ultimate Programming Machine II: Very Dependent Types
by Jason Hickey
November 08, 1994

Seminar The Ultimate Programming Machine
by Jason Hickey
October 25, 1994

Publication 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

Seminar Formalizing the Theory Concept in Nuprl
by Jason Hickey
March 15, 1994

Seminar Formalizing the Theory Mechanism in NuPRL
by Jason Hickey
March 15, 1994

Seminar Abstract Programming in Nuprl
by Jason Hickey
November 23, 1993

Ho, Chi

Publication Byzantine Chain Replication | cite »
by Robbert van Renesse, Chi Ho, Nicolas Schiper
December 20, 2012

Holland-Minkley, Amanda

Seminar Nuprl Library Annotation
by Amanda Holland-Minkley
April 05, 2004

Seminar A Linguistic View of Constuctive Type Theory
by Amanda Holland-Minkley
February 02, 2004

Publication Planning Proof Content for Communicating Induction | cite »
by Amanda Holland-Minkley
2002

Seminar Automatic generation of texts from Nuprl proofs
by Amanda Holland-Minkley
February 04, 2002

Seminar Validating a methodology for natural language generation
by Amanda Holland-Minkley
March 05, 2001

Publication Verbalization of High-Level Formal Proofs | cite »
by Amanda Holland-Minkley, Regina Barzilay, Robert L. Constable
1999

Seminar Verbalization of High-Level Formal Proofs
by Amanda Holland-Minkley
February 01, 1999

Horn, Christian

Publication The Oyster-Clam System | cite »
by Alan Bundy, Frank Van Harmelen, Christian Horn, Alan Smaill
1990

Publication The Nuprl Proof Development System | cite »
by Christian Horn
1988

Howe, Douglas J.

Math Book HOL Translation (partial)
by Douglas J. Howe
February 13, 2004

Seminar Importing HOL Theorems into Nuprl
by Douglas J. Howe
July 30, 1998

Publication A type annotation scheme for Nuprl | cite »
by Douglas J. Howe
October 01, 1998

Publication Semantic Foundations for Embedding HOL in Nuprl | cite »
by Douglas J. Howe
1996

Publication Importing Mathematics from HOL into Nuprl | cite »
by Douglas J. Howe
1996

Publication An Operational Approach to Combining Classical Set Theory and Functional Programming Languages | cite »
by Douglas J. Howe, Scott D. Stoller
1994

Publication Reasoning About Functional Programs in Nuprl | cite »
by Douglas J. Howe
1993

Seminar Constructive Algorithms in Nuprl
by Douglas J. Howe
December 01, 1992

Seminar Set Models
by Douglas J. Howe
November 03, 1992

Seminar Structuring Proofs
by Douglas J. Howe, Paul B. Jackson
October 27, 1992

Seminar Fefprl
by Douglas J. Howe, Douglas J. Howe
October 20, 1992

Seminar Fefprl
by Douglas J. Howe, Douglas J. Howe
October 05, 1992

Publication A Simple Type Theory for Reasoning About Functional Programs | cite »
by Douglas J. Howe
1992

Publication Some Normalization Properties of Martin-Lof's Type Theory and Applications | cite »
by David A. Basin, Douglas J. Howe
1991

Publication On computational open-endedness in Martin-Lof's type theory
by Douglas J. Howe
July 15, 1991

Publication The Semantics of Reflected Proof | cite »
by Stuart F. Allen, Robert L. Constable, Douglas J. Howe, William Aitken
1990

Publication Reflecting the Open-Ended Computation System of Constructive Type Theory | cite »
by Robert L. Constable, Stuart F. Allen, Douglas J. Howe
1990

Publication Nuprl as a General Logic | cite »
by Robert L. Constable, Douglas J. Howe
1990

Publication Implementing Metamathematics as an Approach to Automatic Theorem Proving | cite »
by Robert L. Constable, Douglas J. Howe
1990

Publication Equality in Lazy Computation Systems | cite »
by Douglas J. Howe
1989

Publication Automating Reasoning in an Implementation of Constructive Type Theory | cite »
by Douglas J. Howe
1988

Publication Computational Metatheory in Nuprl | cite »
by Douglas J. Howe
1988

Publication The Computational Behaviour of Girard's Paradox | cite »
by Douglas J. Howe
1987

Publication Implementing Number Theory: An Experiment with Nuprl | cite »
by Douglas J. Howe
1987

Seminar Thesis
by Douglas J. Howe
1984-1985

Seminar Theory of Reals
by Douglas J. Howe
1984-1985

Jackson, Paul B.

Math Book Constructive General Algebra
by Paul B. Jackson
August 19, 1999

Math Book Permutations vol. 1
by Paul B. Jackson
August 19, 1999

Math Book Permutations vol. 2
by Paul B. Jackson
August 19, 1999

Math Book Finite Multi-Sets
by Paul B. Jackson
August 19, 1999

Math Book Constructive Factorization Theory
by Paul B. Jackson
August 19, 1999

Seminar Verifying Garbage Collection Algorithms using the PVS Theorem Prover
by Paul B. Jackson
May 07, 1997

Publication Formalizing Automata Theory I: Finite Automata | cite »
by Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe
1996

Publication The Nuprl Proof Development System, Version 4.2 Reference Manual and User's Guide | cite »
by Paul B. Jackson
1996

Publication Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra | cite »
by Paul B. Jackson
1995

Seminar Developing Set Theory in HOL
by Paul B. Jackson
February 28, 1995

Seminar Verifying an Implementation of a Polynomial Algebra ADT
by Paul B. Jackson
November 29, 1994

Publication Towards Integrated Systems for Symbolic Algebra and Formal Constructive Mathematics | cite »
by Robert L. Constable, Paul B. Jackson
1994

Publication Exploring Abstract Algebra in Constructive Type Theory | cite »
by Paul B. Jackson
1994

Seminar The MIZAR Project
by Paul B. Jackson
February 15, 1994

Seminar Defining Polynomials in Constructive Type Theory
by Paul B. Jackson
1992-1993

Seminar Editor Demonstration
by Paul B. Jackson
March 09, 1993

Seminar Structuring Proofs
by Douglas J. Howe, Paul B. Jackson
October 27, 1992

Publication Nuprl and Its Use in Circuit Design | cite »
by Paul B. Jackson
1992

Seminar Nuprl 3 vs. Nuprl 4
by Paul B. Jackson
November 05, 1991

Publication Developing a Toolkit for Floating-Point Hardware in the Nuprl Proof Development System | cite »
by Paul B. Jackson
1991

Seminar Using Nuprl to Verify Floating Point Hardware
by Paul B. Jackson
April 17, 1990

Publication Logic-Based Knowledge Representation | cite »
by Paul B. Jackson
1989

Kamareddine, Fairouz

Publication 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

Math Book An Intuitionistic Formalization of The Elements of Euclid Book I
by Ariel Kellison, Mark Bickford
November 26, 2019

Publication Implementing Euclid's Straightedge and Compass Constructions in Type Theory | cite »
by Ariel Kellison, Mark Bickford, Robert L. Constable
2018

Klavins, Eric

Seminar Some Recent Results in MetaPRL
by Eric Klavins
April 22, 2002

Kleinberg, Jon

Publication A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics | cite »
by Jon Kleinberg, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz
2003

Knight, Brent

Seminar Program Optimization in Type Theory
by Brent Knight
October 18, 1994

Knoblock, Todd B.

Publication Metamathematical Extensibility in Type Theory | cite »
by Todd B. Knoblock
1987

Seminar Metamathematics of Reflection
by Todd B. Knoblock
April 22, 1987

Publication Formalized Metareasoning in Type Theory | cite »
by Todd B. Knoblock, Robert L. Constable
1986

Seminar Reflective PRL
by Todd B. Knoblock
1984-1985

Publication Writing Programs That Construct Proofs | cite »
by Robert L. Constable, Todd B. Knoblock, Joseph L. Bates
1984

Kopylov, Alexei

Publication Type Theoretical Foundations for Data Structures, Classes, and Objects | cite »
by Alexei Kopylov
2004

Seminar Verified Implementation of Red-Black Trees
by Alexei Kopylov
November 10, 2003

Publication Dependent Intersection: A New Way of Defining Records in Type Theory | cite »
by Alexei Kopylov
2003

Seminar Representing Red-Black Trees in MetaPRL
by Alexei Kopylov
March 10, 2003

Seminar Continuing Discussion of Objects
by Alexei Kopylov, Robert L. Constable
December 02, 2002

Seminar Continuing on Objects and Classes
by Alexei Kopylov
November 18, 2002

Seminar Abstact Data Structures, Objects and Classes in the Nuprl Type Theory
by Alexei Kopylov
November 11, 2002

Seminar Representing Objects in Nuplr Type Theory
by Alexei Kopylov
April 29, 2002

Seminar Objects
by Alexei Kopylov
November 19, 2001

Seminar Record calculus
by Alexei Kopylov
November 12, 2001

Publication Markov's Principle For Propositional Type Theory | cite »
by Alexei Kopylov, Aleksey Nogin
2001

Seminar Kopylov and Nogin CSL Submission
by Alexei Kopylov
April 02, 2001

Seminar A complete list of differences between MetaPRL and Nuprl 4 implementations of type theory
by Alexei Kopylov, Aleksey Nogin
November 27, 2000

Seminar A complete list of differences between MetaPRL and Nuprl 4 implementations of type theory (cont)
by Aleksey Nogin, Alexei Kopylov
December 04, 2000

Seminar Intersections, Unions and Games
by Robert L. Constable, Alexei Kopylov, Aleksey Nogin
December 06, 1999

Seminar Decidability of Linear Affine Logic
by Alexei Kopylov
November 01, 1999

Seminar Linear Logic
by Alexei Kopylov
October 18, 1999

Kozen, Dexter

Math Book Formalizing Moessner's Theorem in Nuprl
by Mark Bickford, Dexter Kozen, Alexandra Silva
June 08, 2012

Publication Automating Proofs in Category Theory | cite »
by Dexter Kozen, Christoph Kreitz, Eva Richter
2006

Seminar A Proof-Theoretic Approach to Knowledge Acquisition"
by Dexter Kozen
January 28, 2002

Kreitz, Christoph

Seminar Wider Deployment of Nuprl
by Richard Eaton, Mark Bickford, Robert L. Constable, Christoph Kreitz
September 28, 2012

Publication Nuprl as Logical Framework for Automating Proofs in Category | cite »
by Christoph Kreitz
April 26, 2012

Publication Introduction to Classic ML | cite »
by Christoph Kreitz, Vincent Rahli
2011

Publication 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

Publication Automating Proofs in Category Theory | cite »
by Dexter Kozen, Christoph Kreitz, Eva Richter
2006

Seminar Microsoft's Spec#
by Christoph Kreitz
April 17, 2006

Seminar Constructive Proofs and Program Extraction
by Christoph Kreitz
February 23, 2004

Publication A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics | cite »
by Jon Kleinberg, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz
2003

Publication The FDL Navigator: Browsing and Manipulating Formal Content | cite »
by Christoph Kreitz
2003

Seminar The Calculemus Autumn School
by Christoph Kreitz, Sabina Petride, Matthew Fluet
October 28, 2002

Publication FDL: A Prototype Formal Digital Library
by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2002

Seminar Enhancing Proof Assistant Systems
by Christoph Kreitz
February 25, 2002

Seminar Embedded Ststems
by Christoph Kreitz, Robert L. Constable
November 05, 2001

Seminar Proof Automation in Constructive Type Theory
by Christoph Kreitz
September 17, 2001

Publication An Experiment in Formal Design Using Meta-Properties | cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Robert L. Constable
2001

Publication Proving Hybrid Protocols Correct | cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu
2001

Publication Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment | cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse
2001

Publication Connection-Driven Inductive Theorem Proving | cite »
by Christoph Kreitz, Brigitte Pientka
2001

Publication Protocol Switching: Exploiting Meta-Properties | cite »
by Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable
2001

Publication JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants | cite »
by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin
2001

Publication The Nuprl Open Logical Environment | cite »
by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2000

Publication Matrix-Based Constructive Theorem Proving | cite »
by Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka
2000

Publication Matrix-Based Inductive Theorem Proving | cite »
by Christoph Kreitz, Brigitte Pientka
2000

Publication A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems | cite »
by Christoph Kreitz, Stephan Schmitt
2000

Publication Dependence Analysis Through Type Inference | cite »
by Ozan Hafizogullari, Christoph Kreitz
1999

Publication Connection-Based Theorem Proving in Classical and Non-Classical Logics | cite »
by Christoph Kreitz, Jens Otten
1999

Publication Automated Fast-Track Reconfiguration of Group Communication Systems | cite »
by Christoph Kreitz
1999

Publication Automating Inductive Specification Proofs | cite »
by Brigitte Pientka, Christoph Kreitz
1999

Publication A Proof Environment for the Development of Group Communication Systems | cite »
by Christoph Kreitz, Mark Hayden, Jason Hickey
1998

Publication Formal Reasoning About Communication Systems II: Automated Fast-Track Reconfiguration | cite »
by Christoph Kreitz
1998

Publication A Matrix Characterization for MELL | cite »
by Heiko Mantel, Christoph Kreitz
1998

Publication Instantiation of Existentially Quantified Variables in Inductive Specification Proofs | cite »
by Brigitte Pientka, Christoph Kreitz
1998

Seminar Dead Code Elimination
by Ozan Hafizogullari, Christoph Kreitz
January 27, 1998

Publication Formal Reasoning About Communication Systems I: Embedding ML in Type Theory | cite »
by Christoph Kreitz
1997

Seminar Formal Reasoning about Communication Systems
by Christoph Kreitz
1996-1997

Publication Meta-Synthesis: Deriving Programs That Develop Programs | cite »
by Christoph Kreitz
1992

Publication Constructive Automata Theory Implemented with the Nuprl Proof Development System | cite »
by Christoph Kreitz
1986

Laan, Twan

Publication Russell's Orders in Kripke's Theory of Truth and Computational Type Theory | cite »
by Robert L. Constable, Fairouz Kamareddine, Twan Laan
2012

Lawall, Julia

Seminar Proofs by Structural Induction using Partial Evaluation
by Julia Lawall
April 13, 1993

Leeser, Miriam

Publication 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

Publication Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification | cite »
by Mark Aagaard, Miriam Leeser
1993

Publication Using Nuprl for the Verification and Synthesis of Hardware | cite »
by Miriam Leeser
1992

Publication Formally Verified Synthesis of Combinational Circuits | cite »
by David A. Basin, Geoffrey Brown, Miriam Leeser
1991

Leino, Rustan

Seminar DEC
by Rustan Leino
November 19, 1996

Lipton, Jim

Seminar Can we Compile the Prolog Program to a Type?
by Jim Lipton
November 12, 1991

Seminar Plotkin
by Jim Lipton
March 13, 1990

Seminar Logical Relations
by Jim Lipton
March 06, 1990

Seminar Intuitionistic ZF
by Jim Lipton
January 30, 1990

Seminar Realizabiity for IZF
by Jim Lipton
March 12, 1987

Seminar IZF and Recursive Realizability
by Jim Lipton
March 05, 1987

Liu, Annie

Seminar A Program Transformation System
by Annie Liu
1993-1994

Liu, Xiaoming

Publication Proving Hybrid Protocols Correct | cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu
2001

Publication Protocol Switching: Exploiting Meta-Properties | cite »
by Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable
2001

Lorigo, Lori

Publication 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

Publication Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts | cite »
by Stuart F. Allen, Robert L. Constable, Lori Lorigo
2006

Publication Information Management in the Service of Knowledge and Discovery | cite »
by Lori Lorigo
2006

Seminar Enhancing the search of mathematics & Hot topics in mathematical search
by Lori Lorigo
May 03, 2004

Publication MetaPRL -- A Modular Logical Environment | cite »
by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo
2003

Publication FDL: A Prototype Formal Digital Library
by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2002

Seminar Report on the DARPA PCES PI meeting
by Robert L. Constable, Lori Lorigo, Mark Bickford
October 29, 2001

Publication JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants | cite »
by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin
2001

Publication The Nuprl Open Logical Environment | cite »
by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2000

Luchangco, Victor

Seminar A Formal Framework for Modeling Memory
by Victor Luchangco
February 22, 1999

Lynch, Nancy

Publication Specifications and Proofs for Ensemble Layers | cite »
by Jason Hickey, Nancy Lynch, Robbert van Renesse
1999

Madden, Peter

Publication Automatic Program Optimization Via the Transformation of Nuprl Synthesis Proofs | cite »
by Peter Madden
1988

Mannion, Conal

Seminar Notation and Computer Aided Mathematics
by Conal Mannion
December 06, 1994

Seminar Reasoning about Scientific Programs
by Conal Mannion, Stuart F. Allen
1993-1994

Seminar Formalizing Hamiltonian Dynamics
by Conal Mannion
November 09, 1993

Manohar, Rajit

Seminar A Methodology for Designing Asynchronous Circuits
by Rajit Manohar
May 10, 1999

Mantel, Heiko

Seminar Principles of Stepwise Refinement
by Heiko Mantel
November 22, 1999

Publication A Matrix Characterization for MELL | cite »
by Heiko Mantel, Christoph Kreitz
1998

Mayr, Tobias

Seminar SupInf
by Tobias Mayr
September 23, 1997

McAllister, David

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
May 04, 1993

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
April 08, 1988

Seminar TBA
by David A. Basin, David McAllister, Wilfred Z. Chen
October 13, 1987

Seminar The ONTIC System
by David McAllister
October 06, 1987

Melis, Erica

Seminar Proof presentation in the Omega system
by Erica Melis
October 25, 1999

Seminar Knowledge-Based Proof Planning
by Erica Melis
April 19, 1999

Mendler, Nax P.

Seminar M-L Type Theory, Categories, Inductive Types
by Nax P. Mendler
1990 Summ

Seminar Polymorphism Is Not Set Theoretic
by Nax P. Mendler
February 14, 1990

Publication Inductive Definition in Type Theory | cite »
by Nax P. Mendler
1988

Publication Recursive Types and Type Constraints in Second-Order Lambda Calculus | cite »
by Nax P. Mendler
1987

Seminar Strong Normalization in Lambda²
by Nax P. Mendler
October 02, 1986

Publication Infinite Objects in Type Theory | cite »
by Nax P. Mendler, Robert L. Constable, Prakash Panangaden
1986

Publication Recursive Definitions in Type Theory | cite »
by Robert L. Constable, Nax P. Mendler
1985

Seminar PP-lambda in Nuprl
by Nax P. Mendler
1984-1985

Seminar Denotational Semantics
by Nax P. Mendler
1984-1985

Seminar Partial Recursive Functions
by Nax P. Mendler
1984-1985

Misra, Jaydev

Seminar Structured Concurrent Programming
by Jaydev Misra
September 15, 2006

Mitchell, John

Seminar Empty Types
by John Mitchell
September 25, 1986

Moczydlowski, Wojciech

Publication Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus | cite »
by Wojciech Moczydlowski, Robert L. Constable
2007

Publication A Dependent Set Theory
by Wojciech Moczydlowski
2007

Publication Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics | cite »
by Robert L. Constable, Wojciech Moczydlowski
2006

Publication A Normalizing Intuitionistic Set Theory with Inaccessible Sets | cite »
by Wojciech Moczydlowski
2006

Publication Normalization of intuitionistic set theories. | cite »
by Wojciech Moczydlowski
2006

Publication Termination of Single-Threaded One-rule Semi-Thue Systems | cite »
by Wojciech Moczydlowski, Alfons Geser
2005

Seminar Extraction in IZF
by Wojciech Moczydlowski
February 25, 2005

Seminar Set-theoretical models of type theory (cont.)
by Wojciech Moczydlowski
September 20, 2004

Seminar Set-theoretical models of type theory
by Wojciech Moczydlowski
September 13, 2004

Seminar (Constructive) set-theoretic semantics for (Constructive) higher-order logic
by Wojciech Moczydlowski
November 04, 2005

Seminar Coq and Nuprl
by Wojciech Moczydlowski
July 27, 2004

Moore, J Strother

Seminar An ACL2 Demo
by J Strother Moore
October 07, 2002

Moran, Evan

Seminar Order-theoretic Differences Between Two Variants of Type Theory
by Evan Moran
October 19, 2012

Publication 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

Seminar Unions and Unboxed Quotients
by Evan Moran
September 23, 2005

Seminar Non-existence of Unions
by Evan Moran
March 04, 2005

Seminar Separativeness and the Structure of the Singletons
by Evan Moran
October 18, 2004

Seminar Reversing Howe's Substitution Rule
by Evan Moran
September 27, 2004

Seminar Uniform Inhabitants for the Non-Union Blueprints, continued
by Evan Moran
October 28, 2005

Seminar (Re-)Introduction to Howe's Framework, continued
by Evan Moran
October 14, 2005

Seminar (Re-)Introduction to Howe's Framework
by Evan Moran
September 30, 2005

Seminar CFZ From Below (continued)
by Evan Moran
April 19, 2004

Seminar CFZ From Below
by Evan Moran
April 12, 2004

Seminar Discussion of Methods of Sharing Formal Mathematics
by Evan Moran
September 22, 2003

Seminar Bridges Between Set Theory and Type Theory
by Evan Moran
September 15, 2003

Seminar On Howe's Importation of HOL into Nuprl
by Evan Moran
September 29, 1998

Seminar Adding Intersection Types to Doug Howe's Classical Set-Theoretic Semantics
by Evan Moran
April 07, 1998

Seminar CZF, Type Theory, and Nuprl-Light (continued)
by Evan Moran
April 08, 1997

Seminar CZF, Type Theory, and Nuprl-Light
by Evan Moran
April 01, 1997

Moschovakis, Joan Rand

Math Book Intuitionistic Mathematics and Logic
by Joan Rand Moschovakis, Garyfallia Vafeiadou
January 25, 2020

Publication Intuitionistic Mathematics and Logic
by Joan Rand Moschovakis, Garyfallia Vafeiadou
January 25, 2020

Mota, Francisco

Seminar Constructive Topology - A Theory of Observation
by Francisco Mota
October 15, 2014

Seminar Synthetic Topology in NuPRL
by Francisco Mota, Mark Bickford
December 03, 2014

Moten, Roderick

Publication Concurrent Refinement in Nuprl | cite »
by Roderick Moten
1997

Seminar Design of the Nuprl Refiner
by Roderick Moten
September 26, 1995

Seminar The Refiner as the Inference Mechanism of Nuprl Proof Development System
by Roderick Moten
April 04, 1995

Seminar Tactic Trees in eXene
by Roderick Moten
September 22, 1992

Murthy, Chetan

Seminar Chet Says Good-Bye: Theory; Implementation (System); Methodology; Science
by Chetan Murthy
February 14, 1995

Seminar The Engineering Aspects of Proof-Environment Design
by Chetan Murthy
January 24, 1995

Seminar TLA
by Scott D. Stoller, Chetan Murthy
November 01, 1994

Seminar A (Possibly) New Scheme for Libraries/Proof-Contexts
by Chetan Murthy
September 03, 1993

Publication A Computational Analysis of Girard's Translation and LC | cite »
by Chetan Murthy
1992

Publication Finding Computational Content from Classical Proofs | cite »
by Robert L. Constable, Chetan Murthy
1991

Publication An Evaluation Semantics for Classical Proofs | cite »
by Chetan Murthy
1991

Publication A Constructive Proof of Higman's Lemma | cite »
by Chetan Murthy, James R. Russell
1990

Publication Extracting Constructive Content from Classical Proofs | cite »
by Chetan Murthy
1990

Naumov, Pavel

Math Book Zeno
by Pavel Naumov
January 25, 2002

Math Book Simple Imperative Programming
by Pavel Naumov
February 26, 2002

Seminar Importing Isabelle Formal Mathematics into NuPRL
by Pavel Naumov
March 08, 1999

Seminar iPRL: A General Approach to Interpreting Isabelle Results in NuPRL
by Pavel Naumov
September 08, 1998

Publication Formalizing Reference Types in Nuprl | cite »
by Pavel Naumov
1998

Seminar Presenting Semantics for a Fragment of the Java Programming Language in Nuprl Proof Development System
by Pavel Naumov
March 10, 1998

Seminar References in Type Theory
by Pavel Naumov
November 25, 1997

Seminar Reasoning about Java Classes in Nuprl (continued)
by Pavel Naumov
September 16, 1997

Seminar Reasoning about Java Classes in Nuprl
by Pavel Naumov
September 09, 1997

Math Book Turing Machine Basics
by Pavel Naumov
November 01, 1996

Publication Formalizing Automata Theory I: Finite Automata | cite »
by Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe
1996

Publication Formalizing Automata II: Decidable Properties | cite »
by Robert L. Constable, Pavel Naumov
1996

Nogin, Aleksey

Publication MetaPRL -- A Modular Logical Environment | cite »
by Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian Aydemir, Eli Barzilay, Lori Lorigo
2003

Publication Formal Compiler Implementation in a Logical Framework | cite »
by Jason Hickey, Aleksey Nogin
2003

Publication Quotient Types: A Modular Approach | cite »
by Aleksey Nogin
2002

Seminar Review of Theorem Provers Outside Cornell part 2
by Aleksey Nogin
February 18, 2002

Seminar Review of Theorem Provers Outside Cornell part 1
by Aleksey Nogin
February 11, 2002

Seminar Is a type uniquely determined by its equivalence relation?
by Aleksey Nogin
November 26, 2001

Seminar Trip Report
by Aleksey Nogin
October 22, 2001

Seminar Markov's Principle for Propositional Type Theory
by Aleksey Nogin
August 20, 2001

Publication Markov's Principle For Propositional Type Theory | cite »
by Alexei Kopylov, Aleksey Nogin
2001

Publication Writing Constructive Proofs Yielding Efficient Extracted Programs | cite »
by Aleksey Nogin
2001

Publication JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants | cite »
by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin
2001

Seminar Modular approach to formalization of the quotient types
by Aleksey Nogin
April 23, 2001

Seminar Modular approach to quotient and other types
by Aleksey Nogin
April 16, 2001

Seminar New modular approach to formalizing complex types in type theory
by Aleksey Nogin
April 09, 2001

Seminar Internalizing proofs and provability
by Aleksey Nogin
February 19, 2001

Seminar A complete list of differences between MetaPRL and Nuprl 4 implementations of type theory
by Alexei Kopylov, Aleksey Nogin
November 27, 2000

Seminar A complete list of differences between MetaPRL and Nuprl 4 implementations of type theory (cont)
by Aleksey Nogin, Alexei Kopylov
December 04, 2000

Publication Fast Tactic-Based Theorem Proving | cite »
by Jason Hickey, Aleksey Nogin
2000

Seminar Intersections, Unions and Games
by Robert L. Constable, Alexei Kopylov, Aleksey Nogin
December 06, 1999

Seminar Differences between the MetaPRL type theory and the Nuprl type theory
by Aleksey Nogin
April 10, 2000

Seminar Efficient Programming by Extract in Nuprl Type Theory - Continued
by Aleksey Nogin
February 14, 2000

Seminar Efficient Programming by Extract in Nuprl Type Theory
by Aleksey Nogin
February 07, 2000

Seminar The Status of the Meta-Prl Project
by Aleksey Nogin
October 04, 1999

Seminar The Current Projects of the MetaPRL Group
by Aleksey Nogin, Jason Hickey
April 26, 1999

Seminar Speeding Up the MetaPRL Refiner
by Aleksey Nogin
February 08, 1999

Seminar Formal Models for Nuprl Evaluator
by Aleksey Nogin
March 24, 1998

Nogina, Elena

Seminar On continuity of computable real functions
by Elena Nogina
May 01, 2000

O'Donnell, Michael J.

Seminar Connecting Formal Semantics to Constructive Intuitions
by Michael J. O'Donnell
July 06, 1993

Publication A Programming Logic | cite »
by Robert L. Constable, Michael J. O'Donnell
1978

O'Leary, John

Publication 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

Publication Matrix-Based Constructive Theorem Proving | cite »
by Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka
2000

Publication Connection-Based Theorem Proving in Classical and Non-Classical Logics | cite »
by Christoph Kreitz, Jens Otten
1999

Seminar Efficient Automated Proof Search and Proof Reconstruction in Intuitionistic Logic
by Jens Otten, Stephan Schmitt
June 23, 1998

Panangaden, Prakash

Publication Infinite Objects in Type Theory | cite »
by Nax P. Mendler, Robert L. Constable, Prakash Panangaden
1986

Paulin-Mohring, Christine

Seminar Recursive Types in Coq
by Christine Paulin-Mohring
September 08, 1994

Petride, Sabina

Publication Knowledge-based synthesis of distributed systems using event structures | cite »
by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2005

Publication Knowledge-Based Synthesis of Distributed Systems Using Event Structures
by Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride
2004

Seminar Uri Abraham's Models for Concurrency
by Robert L. Constable, Sabina Petride
January 27, 2003

Seminar The Calculemus Autumn School
by Christoph Kreitz, Sabina Petride, Matthew Fluet
October 28, 2002

Pientka, Brigitte

Publication Connection-Driven Inductive Theorem Proving | cite »
by Christoph Kreitz, Brigitte Pientka
2001

Publication Matrix-Based Constructive Theorem Proving | cite »
by Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka
2000

Publication Matrix-Based Inductive Theorem Proving | cite »
by Christoph Kreitz, Brigitte Pientka
2000

Publication Automating Inductive Specification Proofs | cite »
by Brigitte Pientka, Christoph Kreitz
1999

Publication Instantiation of Existentially Quantified Variables in Inductive Specification Proofs | cite »
by Brigitte Pientka, Christoph Kreitz
1998

Seminar Instantiation of Existentially Quantified Variables in Inductive Specification Proofs
by Brigitte Pientka
May 05, 1998

Seminar A Uniform Rippling Approach for Instantiating Free Variables
by Brigitte Pientka
December 02, 1997

Pingali, Keshav

Seminar Distributed Snapshot Algorithms
by Keshav Pingali
February 17, 2003

Publication Collaborative Mathematics Environments | cite »
by Robert L. Constable, Paul Chew, Keshav Pingali, Steve Vavasis, Richard Zippel
1996

Poernomo, Iman

Seminar Adapting Proofs-as-Programs for the Synthesis of Imperative SML Programs
by Iman Poernomo
December 08, 2003

Poetzsch, Arnd

Seminar Formalizing Program Synthesis
by Arnd Poetzsch
April 27, 1993

Rahli, Vincent

Publication Open Bar -- A Reconciliation between Intuitionistic and Classical Logic
by Vincent Rahli, Mark Bickford, Robert L. Constable, Liron Cohen
2020

Publication Bar Induction is Compatible with Constructive Type Theory | cite »
by Vincent Rahli, Liron Cohen, Mark Bickford, Robert L. Constable
2019

Publication Validating Brouwerâ€™s Continuity Principle for Numbers Using Named Exceptions | cite »
by Vincent Rahli, Mark Bickford
January 02, 2018

Publication Computability Beyond Church-Turing using Choice Sequences | cite »
by Liron Cohen, Vincent Rahli, Mark Bickford, Robert L. Constable
2018

Publication A Verified Theorem Prover Backend Supported by a Monotonic Library | cite »
by Vincent Rahli, Liron Cohen, Mark Bickford
November 01, 2018

Publication Bar Induction: The Good, the Bad, and the Ugly | cite »
by Vincent Rahli, Mark Bickford, Robert L. Constable
April 11, 2017

Publication A Nominal Exploration of Intuitionism
by Vincent Rahli, Mark Bickford
January 18, 2016

Publication Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EventML
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
September 01, 2015

Publication Coq as a Metatheory for Nuprl with Bar Induction
by Vincent Rahli, Mark Bickford
September 14, 2015

Publication Nuprlâ€™s Inductive Logical Forms
by Mark Bickford, Robert L. Constable, Richard Eaton, Vincent Rahli
September 01, 2015

Seminar A Type Theory with Partial Equivalence Relations as Types
by Vincent Rahli
September 10, 2014

Seminar Nominal Type Theory
by Mark Bickford, Vincent Rahli
October 29, 2014

Publication Developing Correctly Replicated Databases Using Formal Tools
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
June 23, 2014

Publication A Type Theory with Partial Equivalence Relations as Types
by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli
May 12, 2014

Publication Towards a Formally Verified Proof Assistant
by Abhishek Anand, Vincent Rahli
July 14, 2014

Publication A Generic Approach to Proofs about Substitution
by Abhishek Anand, Vincent Rahli
July 17, 2014

Seminar There Are No Discontinuous Real Functions
by Mark Bickford, Vincent Rahli
October 08, 2014

Publication Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types | cite »
by Vincent Rahli, Mark Bickford, Abhishek Anand
April 22, 2013

Publication Formal Specification, Verification, and Implementation of Fault-Tolerant Systems
by Vincent Rahli, David Guaspari, Mark Bickford, Robert L. Constable
March 31, 2013

Seminar A verified proof assistant
by Vincent Rahli, Abhishek Anand
October 30, 2013

Seminar How far can we go with Induction-Recursion?
by Abhishek Anand, Vincent Rahli
November 20, 2013

Publication Interfacing with Proof Assistants for Domain Specific Programming Using EventML | cite »
by Vincent Rahli
July 11, 2012

Publication 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

Publication The Logic of Events, a framework to reason about distributed systems | cite »
by Mark Bickford, Vincent Rahli, Robert L. Constable
2012

Publication 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

Seminar Simple Consensus Algorithm
by Robert L. Constable, Mark Bickford, Vincent Rahli
October 28, 2011

Publication Introduction to Classic ML | cite »
by Christoph Kreitz, Vincent Rahli
2011

Publication Investigations in intersection types:Confluence, and semantics of expansion in the lambda-calculus, and a type error slicing method | cite »
by Vincent Rahli
2011

Reitblatt, Mark

Seminar ACL2 Tutorial
by Mark Reitblatt
March 27, 2014

Seminar Recent work with Coq
by Mark Reitblatt
May 11, 2012

Remidde, Ettore

Seminar GOLEM
by Ettore Remidde
October 24, 1995

Richter, Eva

Publication Automating Proofs in Category Theory | cite »
by Dexter Kozen, Christoph Kreitz, Eva Richter
2006

Rodeh, Ohad

Rowe, Reuben

Publication Automated Reasoning in Herbrand Structures
by Liron Cohen, Reuben Rowe, Yoni Zohar
June 03, 2019

Publication Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent | cite »
by Liron Cohen, Reuben Rowe
July 01, 2018

Russell, James R.

Publication A Constructive Proof of Higman's Lemma | cite »
by Chetan Murthy, James R. Russell
1990

Sasaki, James T.

Publication Extracting Efficient Code from Constructive Proofs | cite »
by James T. Sasaki
1985

Seminar Optimizing Ext
by James T. Sasaki
1984-1985

Schiper, Nicolas

Publication Developing Correctly Replicated Databases Using Formal Tools
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
June 23, 2014

Publication 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

Publication 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

Publication Byzantine Chain Replication | cite »
by Robbert van Renesse, Chi Ho, Nicolas Schiper
December 20, 2012

Schlimm, Dirk

Seminar Intuitionism - The Philosophy of L. E. J. Brouwer
by Dirk Schlimm
April 24, 1998

Schmitt, Stephan

Publication JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants | cite »
by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin
2001

Publication Matrix-Based Constructive Theorem Proving | cite »
by Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka
2000

Publication A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems | cite »
by Christoph Kreitz, Stephan Schmitt
2000

Seminar An Efficient Refiner for First-order Intuitionistic Logic (Part II)
by Stephan Schmitt
May 22, 2000

Seminar An Efficient Refiner for First-order Intuitionistic Logic
by Stephan Schmitt
February 28, 2000

Seminar Efficient Automated Proof Search and Proof Reconstruction in Intuitionistic Logic
by Jens Otten, Stephan Schmitt
June 23, 1998

Schwartzbach, Michael

Seminar Continuation of Categorial Models of Nuprl
by Michael Schwartzbach
October 28, 1986

Seminar Categorical Models of Nuprl
by Michael Schwartzbach
October 21, 1986

Schwichtenberg, Helmut

Seminar Program Development for Proof Transformations
by Helmut Schwichtenberg
October 12, 1994

Seminar Are There Long Reduction Sequences with Short Normal Forms?
by Helmut Schwichtenberg
September 29, 1992

Sernaker, Sarah

Math Book A Formal Exploration of Constructive Geometry
by Sarah Sernaker, Robert L. Constable
2016

Publication A Formal Exploration of Constructive Geometry
by Robert L. Constable, Sarah Sernaker
2016

Math Book Constructive Reading of Classical Logic
by Robert L. Constable, Sarah Sernaker
2015

Shan, Chung-chieh

Seminar Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
by Chung-chieh Shan
December 02, 2011

Shankar, N

Seminar PVS
by N Shankar
March 24, 1992

Shvartsman, Alex

Seminar A Reconfigurable Atomic Memory Service for Dynamic Networks
by Alex Shvartsman
March 24, 2003

Silva, Alexandra

Math Book Formalizing Moessner's Theorem in Nuprl
by Mark Bickford, Dexter Kozen, Alexandra Silva
June 08, 2012

Smaill, Alan

Publication The Oyster-Clam System | cite »
by Alan Bundy, Frank Van Harmelen, Christian Horn, Alan Smaill
1990

Publication Reflection in Constructive and Non-Constructive Automated Reasoning | cite »
by Fausto Giunchiglia, Alan Smaill
1989

Smith, Scott F.

Publication Partial Objects in Type Theory | cite »
by Scott F. Smith
1989

Publication Computational Foundations of Basic Recursive Function Theory | cite »
by Robert L. Constable, Scott F. Smith
1988

Seminar Partial Objects
by Scott F. Smith
November 24, 1987

Seminar Domains in Type Theory
by Scott F. Smith
November 10, 1987

Publication Partial Objects in Constructive Type Theory | cite »
by Scott F. Smith, Robert L. Constable
1987

Seminar Bar Types
by Scott F. Smith
March 18, 1987

Seminar Term Model Semantics and Tait Computability Method
by Scott F. Smith
March 11, 1987

Seminar Defining Lambda-prl and Its Extensions
by Scott F. Smith
1984-1985

Smolka, Steffen

Seminar Isabelle Tutorial
by Steffen Smolka
March 18, 2014

Stansifer, Ryan

Seminar Marhew's Principle
by Ryan Stansifer
1984-1985

Seminar Prolog
by Ryan Stansifer, Stuart F. Allen
1984-1985

Stehr, Mark-Oliver

Seminar Justifying the HOL-Nuprl Connection in the Categorical Framework of General Logics and Type Theory in a Membership Equational Logic Framework
by Mark-Oliver Stehr
1998-1999

Stevens, Andrew

Seminar 20BJ as a Meta-logical Framework
by Andrew Stevens
April 21, 1990

Seminar Rational Reconstruction of Boyer and Moore Prover
by Andrew Stevens
December 01, 1987

Stoller, Scott D.

Seminar TLA
by Scott D. Stoller, Chetan Murthy
November 01, 1994

Publication An Operational Approach to Combining Classical Set Theory and Functional Programming Languages | cite »
by Douglas J. Howe, Scott D. Stoller
1994

Seminar An Operational Approach to Combining Classical Set Theory and Functional Programming Languages
by Scott D. Stoller
March 29, 1994

Seminar How to Integrate Set Theory and Computation?
by Scott D. Stoller
September 14, 1993

Seminar Semantics
by Scott D. Stoller
March 30, 1993

Seminar Semantics of the Nuprl Type Theory
by Scott D. Stoller
March 16, 1993

Stump, Aarong

Seminar Proof Tools and Correct Program Development
by Aarong Stump
February 03, 2003

Tate, Ross

Seminar Issues in Constructive Type Theory
by Ross Tate
September 14, 2012

Trostle, Anne

Math Book Finding the Maximum Segment Sum
by Anne Trostle
January 22, 2014

Math Book A Fast Algorithm for the Integer Square Root
by Anne Trostle, Mark Bickford
June 09, 2014

Math Book Logical Investigations, with the Nuprl Proof Assistant
by Robert L. Constable, Anne Trostle
July 22, 2014

Math Book An Algorithm for the Greatest Common Divisor
by Anne Trostle
October 01, 2013

Underwood, Judith

Publication Search Algorithms in Type Theory | cite »
by James L. Caldwell, Ian Gent, Judith Underwood
2000

Publication Metalogical Frameworks II: Developing a Reflected Decision Procedure | cite »
by William Aitken, Robert L. Constable, Judith Underwood
1999

Publication Classical Tools for Constructive Proof Search | cite »
by James L. Caldwell, Judith Underwood
1996

Publication Aspects of the Computational Content of Proofs | cite »
by Judith Underwood
1994

Seminar A Constructive Completeness Proof for Intuitionistic Predicate Calculus
by Judith Underwood
February 01, 1994

Publication The Tableau Algorithm for Intuitionistic Propositional Calculus as a Constructive Completeness Proof | cite »
by Judith Underwood
1993

Seminar Extraction
by Judith Underwood
March 16, 1993

Publication A Constructive Completeness Proof for the Intuitionistic Propositional Calculus | cite »
by Judith Underwood
1990

Uribe, Juan

Publication Formalizing Automata Theory I: Finite Automata | cite »
by Robert L. Constable, Paul B. Jackson, Pavel Naumov, Juan Uribe
1996

Vafeiadou, Garyfallia

Publication Intuitionistic Mathematics and Logic
by Joan Rand Moschovakis, Garyfallia Vafeiadou
January 25, 2020

Math Book Intuitionistic Mathematics and Logic
by Joan Rand Moschovakis, Garyfallia Vafeiadou
January 25, 2020

van Dalen, Dirk

Seminar L. E. J. Brouwer's Intuitionism: A Revolution in Two Installments
by Dirk van Dalen
June 26, 1998

van Renesse, Robbert

Publication Developing Correctly Replicated Databases Using Formal Tools
by Nicolas Schiper, Vincent Rahli, Robbert van Renesse, Mark Bickford, Robert L. Constable
June 23, 2014

Publication 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

Publication 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

Publication Byzantine Chain Replication | cite »
by Robbert van Renesse, Chi Ho, Nicolas Schiper
December 20, 2012

Publication Investigating Correct-by-Construction Attack-Tolerant Systems | cite »
by Robert L. Constable, Mark Bickford, Robbert van Renesse
2010

Publication An Experiment in Formal Design Using Meta-Properties | cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Robert L. Constable
2001

Publication Proving Hybrid Protocols Correct | cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu
2001

Publication Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment | cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse
2001

Publication Protocol Switching: Exploiting Meta-Properties | cite »
by Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable
2001

Publication Specifications and Proofs for Ensemble Layers | cite »
by Jason Hickey, Nancy Lynch, Robbert van Renesse
1999

Vardi, Moshe

Seminar A Conversation with Moshe Vardi
by Moshe Vardi
November 18, 2011

Vavasis, Steve

Publication Collaborative Mathematics Environments | cite »
by Robert L. Constable, Paul Chew, Keshav Pingali, Steve Vavasis, Richard Zippel
1996

Vogels, Werner

Walker, David

Seminar Regions, part 2: The Capability Calculus
by David Walker
November 15, 1999

Seminar An Introduction to Region Inference
by David Walker
November 08, 1999

Weirich, Stephanie

Seminar Intensional Polymorphism in Type-Erasure Semantics
by Stephanie Weirich
April 28, 1998

Werner, Benjamin

Seminar Extraction of Programs
by Benjamin Werner
1993-1994

Wilson, Todd

Seminar Work in Progress: A Formalization of the SUP-INF Algorithm
by Todd Wilson
July 11, 1996

Seminar Some Recent Results of R. Dyckhoff and A. Pitts
by Todd Wilson
March 26, 1996

Seminar Motivation: Basis of a Set Theory for Nuprl
by Todd Wilson
February 21, 1995

Seminar Computer Algebra, Theorem Proving, and Types
by Todd Wilson
October 04, 1994

Wu, Jason

Seminar Transforming Protocols from Shared Memory Models to Message Passing Models Provides a New Source of High Level Synthetic Protocol Diversity
by Jason Wu
November 09, 2012

Seminar A Discussion in Consensus
by Jason Wu
February 10, 2012

Seminar Adding Shared Memory to the General Process Model
by Jason Wu
April 20, 2012

Yan, Thomas

Seminar GrÃ¶bner Basis
by Thomas Yan
September 20, 1994

Seminar Hilbert Basis Function
by Thomas Yan
March 01, 1994

Zippel, Richard

Publication Collaborative Mathematics Environments | cite »
by Robert L. Constable, Paul Chew, Keshav Pingali, Steve Vavasis, Richard Zippel
1996

Seminar The MathBus Term Structure
by Richard Zippel
1995-1996

Zohar, Yoni

Publication Automated Reasoning in Herbrand Structures
by Liron Cohen, Reuben Rowe, Yoni Zohar
June 03, 2019

Knowledge Base of Publications, Seminars, & Math Library

List by Author

Knowledge Base of
Publications, Seminars, & Math Library