Nuprl Basics by
Stuart F. Allen
Subject: Nuprl Description: Basic concepts and methods used for mathematical expressions in Nuprl. The primitive operators as well as basic nonprimitives are discussed.
2003

Standard Resources by
Stuart F. Allen
Subject: Nuprl Description: Standard library of Nuprl objects.
2003

Elementary Number Theory by
Stuart F. Allen
Subject: Arithmetic Description: Elementary divisibility theory over the integers. Gcd function and relation introduced. Chinese remainder theorem proven.
2003

Lists by
Stuart F. Allen
Subject: Description: We emphasize here several sections of the library about the List data type.
2001

Square Root of 2 is Irrational by
Stuart F. Allen
Subject: Arithmetic Description: Here we give formal proofs along with informal glosses of proofs to the effect that 2 has no rational square root, and more generally, that no prime number has a rational square root.
The proof about 2 is simpler, of course, and so is a better approach to the one about primes.
2004

Discrete Math Materials by
Stuart F. Allen
Subject: Arithmetic Description: Counting is finding a function of a certain kind.
When we count a class of objects, we generate an enumeration of them, which we may represent by a onetoone correspondence from a standard class having that many objects to the class being counted. Our standard class of n objects, for n , will be n, which is the class {k: 0 k < n } of natural numbers less than n. A more familiar choice of standard finite classes might have been {k: 1 k n }, but there is also another tradition in math for using {k: 0 k < n }.
2004

Fundamental Theorem of Arithmetic by
Stuart F. Allen
Subject: Arithmetic Description: The Fundamental Theorem of Arithmetic  unique prime factorizability
2004

Iterated Binary Operations by
Stuart F. Allen
Subject: Systems Description: This section treats the iteration of binary operations over values indexed indexed by finite integer subranges. We parameterize iteration by the binary operation and a value, typically its identity element, for the empty range. Here are some familiar special cases.
2004

Russel's Paradox by
Stuart F. Allen
Subject: Logic Description:
2004

How to browse the library by
Stuart F. Allen
Subject: Description:
2004

Towers of Hanoi by
Stuart F. Allen
Subject: Puzzels Description: Towers of Hanoi: a thorough treatment.
The purpose of these notes is to exhibit the application of formal prooforiented methods to a familiar nontrivial problem.
2004

Readability Exercise (num theory) by
Stuart F. Allen
Subject: Arithmetic Description: Number Theory Examples
Here are several examples of proofs about numbers. Each consists of a formal proof and an informal gloss of it.
2004

Nuprl Editor and Interface by
Stuart F. Allen
Subject: Nuprl Description: Editor Documentation from the nuprl_sfa interface to Nuprl4.
2003

Chain Replication Protocol by
Mark Bickford
Subject: Systems Description: This book collects materials used in the formalization of an important distributed algorithm, by Schneider and van Renesse, called Chain Replication. The chain replication algorithm provides a faulttolerant distributed storage system and guarantees a strong consistency property.
2006

Event Systems by
Mark Bickford
Subject: Systems Description: This is Mark Bickford's formal library about the Event Systems developed by him and Robert Constable.
2003

Graph Theory by
Mark Bickford
Subject: Description: This is Mark Bickford's formal library about the Graph Theory.
2003

Hybrid Protocols by
Mark Bickford
Subject: Systems Description: We describe a generic switching protocol for the construction of hybrid protocols and prove it correct with the proof development system. We introduce the concept of metaproperties to characterize communication properties that can be preserved by switching and identify switching invariants that an implementation of the switching protocol must satisfy in order to work correctly.
2002

Introduction to EventML by
Mark Bickford, Robert L. Constable, Richard Eaton, David Guaspari
Subject: Nuprl Description: EventML is a functional programming language in the ML family, closely related to Classic ML. It is also a language for coding distributed protocols (such as Paxos [Ren11]) using high level combinators from the Logic of Events (or Event Logic), hence the name EventML.
EventML was also created to work in cooperation with an interactive theorem prover and to be a key component of a Logical Programming Environment (LPE).
This tutorial also includes multiple example protocols, including ping pong, 2/3 consensus, and Paxos (coming soon).
2012

General Automata Theory by
Mark Bickford
Subject: Systems Description: General (infinitestate) transition systems are defined using records. This makes it possible to define intersection and renaming operations on the transition systems, which we call statemachines, and these operations have nice properties. We define notions such as reachable states, invariants, stable properties, etc. and prove theorems about their preservation under intersection and renaming.
2003

Formalizing Moessner's Theorem in Nuprl by
Mark Bickford, Dexter Kozen, Alexandra Silva
Subject: Logic Description: Moessner's theorem describes a procedure for generating a sequence of n integer sequences that lead unexpectedly to the sequence of nth powers 1^{n}, 2^{n}, 3^{n}, ... . Several generalizations of Moessner's theorem exist. Recently, Kozen and Silva gave an algebraic proof of a general theorem that subsumes Moessner's original theorem and its know generalizations. In this note, we describe the formalization of this theorem that the first author did in Nuprl.
2012

Formalizing Constructive Analysis in Nuprl by
Mark Bickford
Subject: Arithmetic Description: Mark Bickford has been formalizing Chapter Two of Constructive Analysis in Nuprl, creating detailed definitions and proofs.
2012

A Fast Algorithm for the Integer Square Root by
Anne Trostle, Mark Bickford
Subject: Arithmetic Description: The integer square root of a natural number can be solved using many different algorithms which differ in level of efficiency. We discuss several of these algorithms and include a detailed account of a constructive proof using fast induction. We also introduce the concept of constructive real numbers and relate the integer square root to the real square root.
2014

An Intuitionistic Formalization of The Elements of Euclid Book I by
Ariel Kellison, Mark Bickford
Subject: Geometry Description: A Nuprl formalization of Book I of the Elements of Euclid using intuitionistic primitives and axioms.
2019

Classical Propositional Logic by
James L. Caldwell
Subject: Logic Description: We describe a formal constructive proof of the decidability of a sequent calculus for classical propositional logic. The proof is implemented in the Nuprl system and the resulting proof object yields a correctbyconstruction program for deciding propositional sequents.
2004

Finite Automata by
Robert L. Constable
Subject: Logic Description:
2001

Introduction to EventML by
Mark Bickford, Robert L. Constable, Richard Eaton, David Guaspari
Subject: Nuprl Description: EventML is a functional programming language in the ML family, closely related to Classic ML. It is also a language for coding distributed protocols (such as Paxos [Ren11]) using high level combinators from the Logic of Events (or Event Logic), hence the name EventML.
EventML was also created to work in cooperation with an interactive theorem prover and to be a key component of a Logical Programming Environment (LPE).
This tutorial also includes multiple example protocols, including ping pong, 2/3 consensus, and Paxos (coming soon).
2012

Collaborative Mathematics Environments by
Robert L. Constable
Subject: Systems Description: Written with Paul Chew, Keshav Pingali, Steve Vavasis, Richard Zippel
Computational science will be the dominant paradigm for science in the next century. This proposal addresses one of the major challenges facing this new kind of sciencethe demand for better software support for computational mathematics. The task of providing this support is sufficiently central to the national interest and sufficiently comprehensive that it could serve as a Grand Challenge problem for computer science.
1996

Logical Investigations, with the Nuprl Proof Assistant by
Robert L. Constable, Anne Trostle
Subject: Logic Description: An introduction to concepts in FirstOrder Logic, illustrated using proofs from Nuprl
2014

Constructive Reading of Classical Logic by
Robert L. Constable, Sarah Sernaker
Subject: Description: Using the implementation of virtual evidence, Nuprl can constructively prove classical theorems.
2015

A Formal Exploration of Constructive Geometry by
Sarah Sernaker, Robert L. Constable
Subject: Description: We investigated synthetic geometry and propositions from Euclid's Elements using constructive mathematics and utilizing results from Beeson, Tarski, Hilbert, and Euclid.
2016

BarType Rules by
Karl Crary
Subject: Description:
2002

Automatic FDL Projections by
Richard Eaton
Subject: Nuprl Description: Collection of projections from the Formal Digital Library in 2006
2006

Introduction to EventML by
Mark Bickford, Robert L. Constable, Richard Eaton, David Guaspari
Subject: Nuprl Description: EventML is a functional programming language in the ML family, closely related to Classic ML. It is also a language for coding distributed protocols (such as Paxos [Ren11]) using high level combinators from the Logic of Events (or Event Logic), hence the name EventML.
EventML was also created to work in cooperation with an interactive theorem prover and to be a key component of a Logical Programming Environment (LPE).
This tutorial also includes multiple example protocols, including ping pong, 2/3 consensus, and Paxos (coming soon).
2012

Work in Progress by
Richard Eaton
Subject: Nuprl Description: a snapshot of Nuprl library objects
2012

Introduction to EventML by
Mark Bickford, Robert L. Constable, Richard Eaton, David Guaspari
Subject: Nuprl Description: EventML is a functional programming language in the ML family, closely related to Classic ML. It is also a language for coding distributed protocols (such as Paxos [Ren11]) using high level combinators from the Logic of Events (or Event Logic), hence the name EventML.
EventML was also created to work in cooperation with an interactive theorem prover and to be a key component of a Logical Programming Environment (LPE).
This tutorial also includes multiple example protocols, including ping pong, 2/3 consensus, and Paxos (coming soon).
2012

HOL Translation (partial) by
Douglas J. Howe
Subject: Nuprl Description: This is part of Doug Howe's HOL library.
It modifies the Nuprl logic to make HOL interpretable.
This translation is based upon Howe's Importing Mathematics from HOL into Nuprl.
2004

Constructive General Algebra by
Paul B. Jackson
Subject: Arithmetic Description:
1999

Permutations vol. 1 by
Paul B. Jackson
Subject: Description:
1999

Permutations vol. 2 by
Paul B. Jackson
Subject: Description: Defines several equivalence relations on lists, including 'is a permutation of', 'is a permutation of up to', and 'is equivalent to, up to'.
The permutation relations were defined in terms of permutation functions. This turned out to be rather awkward. Would have been much easier to start with computable notions of when one list is a permutation of another (see list_2 for details).
Various properties of these relations were proven.
1999

Finite MultiSets by
Paul B. Jackson
Subject: Description: Nuprl's quotient type is used to construct a type of finite multisets from the type of lists. Standard functions over multisets are introduced, including a summation function that draws indices from finite multisets.
A definition is given of a free abelian monoid ADT, and an instance of this ADT is constructed using the multiset functions.
Finite sets are defined as a subtype of finite multisets, and the usual set operations are introduced.
1999

Constructive Factorization Theory by
Paul B. Jackson
Subject: Arithmetic Description: Introduces the theory of divisibility in cancellation monoids, and builds up to theorem characterizing when unique factorizations exist and are unique.
The theory here is developed constructively. Some theorems computable content is 'useful': e.g. mfact_exists. An instantiation of this theorem is posint_is_ufm, which has as extract, a theorem to compute prime factorisations. Other theorems have computational content which is for most purposes uninteresting. e.g. look at theorem unique_mfact.
The theorem unique_mfact nicely demonstrates rewriting with equivalence relations of differing strengths: e.g. permr and permr_upto.
1999

An Intuitionistic Formalization of The Elements of Euclid Book I by
Ariel Kellison, Mark Bickford
Subject: Geometry Description: A Nuprl formalization of Book I of the Elements of Euclid using intuitionistic primitives and axioms.
2019

Formalizing Moessner's Theorem in Nuprl by
Mark Bickford, Dexter Kozen, Alexandra Silva
Subject: Logic Description: Moessner's theorem describes a procedure for generating a sequence of n integer sequences that lead unexpectedly to the sequence of nth powers 1^{n}, 2^{n}, 3^{n}, ... . Several generalizations of Moessner's theorem exist. Recently, Kozen and Silva gave an algebraic proof of a general theorem that subsumes Moessner's original theorem and its know generalizations. In this note, we describe the formalization of this theorem that the first author did in Nuprl.
2012

Intuitionistic Mathematics and Logic by
Joan Rand Moschovakis, Garyfallia Vafeiadou
Subject: Intuitionistic Mathematics Description: The first seeds of mathematical intuitionism germinated in Europe over a century ago in the constructive tendencies of Borel, Baire, Lebesque, Poincaré, Kronecker and others. The flowering was the work of one man, Luitzen Egbertus Jan Brouwer, who taught mathematics at the University of Amsterdam from 1909 until 1951. By proving powerful theorems on topological invariants and fixed points of continuous mappings, Brouwer quickly build a mathematical reputation strong enough to support his revolutionary ideas about the nature of mathematical activity. These ideas influenced Hilbert and Gödel and established intuitionistic logic and mathematics as subjects worthy of independent study
Our aim is to describe the development of Brouwer's intuitionism, from his rejection of the classical law of excluded middle to his controversial theory of the continuum, with fundamental consequences for logic and mathematics. We borrow Kleene's formal axiomatic systems (incorporating earlier attempts by Kolmogorov, Glivenko, Heyting and Peano) for intuitionistic logic and arithmetic as subtheories of the corresponding classical theories, and sketch his use of gödel numbers of recursive functions to realize sentences of intuitionistic arithmetic including a form of Church's Thesis. Finally, we present Kleene and Vesley's axiomatic treatment of Brouwer's continuum, with the functionrealizability interpretation which establishes its consistency.
2020

Zeno by
Pavel Naumov
Subject: Description:
2002

Simple Imperative Programming by
Pavel Naumov
Subject: Systems Description: Simple Imperative Programming Language library is a collection of Nuprl theories that formalize syntax and semantics of a simple imperative programming language.
2002

Turing Machine Basics by
Pavel Naumov
Subject: Logic Description:
1996

Constructive Reading of Classical Logic by
Robert L. Constable, Sarah Sernaker
Subject: Description: Using the implementation of virtual evidence, Nuprl can constructively prove classical theorems.
2015

A Formal Exploration of Constructive Geometry by
Sarah Sernaker, Robert L. Constable
Subject: Description: We investigated synthetic geometry and propositions from Euclid's Elements using constructive mathematics and utilizing results from Beeson, Tarski, Hilbert, and Euclid.
2016

Formalizing Moessner's Theorem in Nuprl by
Mark Bickford, Dexter Kozen, Alexandra Silva
Subject: Logic Description: Moessner's theorem describes a procedure for generating a sequence of n integer sequences that lead unexpectedly to the sequence of nth powers 1^{n}, 2^{n}, 3^{n}, ... . Several generalizations of Moessner's theorem exist. Recently, Kozen and Silva gave an algebraic proof of a general theorem that subsumes Moessner's original theorem and its know generalizations. In this note, we describe the formalization of this theorem that the first author did in Nuprl.
2012

An Algorithm for the Greatest Common Divisor by
Anne Trostle
Subject: Arithmetic Description: This page shows existence proofs and recursive algorithms in Nuprl for the greatest common divisor of two natural numbers.
2013

Finding the Maximum Segment Sum by
Anne Trostle
Subject: Arithmetic Description: The problem of finding the maximum segment sum for a given sequence of numbers is useful for illustrating several key concepts in programming, such as writing specifications, utilizing dependent types, and showing how proofs reveal programs and programs reveal proofs. In this account of the problem, we describe an algorithm for finding the solution and then show its proof in Nuprl.
2014

A Fast Algorithm for the Integer Square Root by
Anne Trostle, Mark Bickford
Subject: Arithmetic Description: The integer square root of a natural number can be solved using many different algorithms which differ in level of efficiency. We discuss several of these algorithms and include a detailed account of a constructive proof using fast induction. We also introduce the concept of constructive real numbers and relate the integer square root to the real square root.
2014

Logical Investigations, with the Nuprl Proof Assistant by
Robert L. Constable, Anne Trostle
Subject: Logic Description: An introduction to concepts in FirstOrder Logic, illustrated using proofs from Nuprl
2014

Intuitionistic Mathematics and Logic by
Joan Rand Moschovakis, Garyfallia Vafeiadou
Subject: Intuitionistic Mathematics Description: The first seeds of mathematical intuitionism germinated in Europe over a century ago in the constructive tendencies of Borel, Baire, Lebesque, Poincaré, Kronecker and others. The flowering was the work of one man, Luitzen Egbertus Jan Brouwer, who taught mathematics at the University of Amsterdam from 1909 until 1951. By proving powerful theorems on topological invariants and fixed points of continuous mappings, Brouwer quickly build a mathematical reputation strong enough to support his revolutionary ideas about the nature of mathematical activity. These ideas influenced Hilbert and Gödel and established intuitionistic logic and mathematics as subjects worthy of independent study
Our aim is to describe the development of Brouwer's intuitionism, from his rejection of the classical law of excluded middle to his controversial theory of the continuum, with fundamental consequences for logic and mathematics. We borrow Kleene's formal axiomatic systems (incorporating earlier attempts by Kolmogorov, Glivenko, Heyting and Peano) for intuitionistic logic and arithmetic as subtheories of the corresponding classical theories, and sketch his use of gödel numbers of recursive functions to realize sentences of intuitionistic arithmetic including a form of Church's Thesis. Finally, we present Kleene and Vesley's axiomatic treatment of Brouwer's continuum, with the functionrealizability interpretation which establishes its consistency.
2020
