Nuprl - MaRDI portal

Cited in

(only showing first 100 items - show all)

Proof assistants: history, ideas and future
Formalizing Arrow's theorem
Continuity and Lipschitz constants for projections
8th international conference on automated deduction, Oxford, England, July 27 -- August 1, 1986. Proceedings
Constructing recursion operators in intuitionistic type theory
On the syntax of Martin-Löf's type theories
Terminating general recursion
On Church's formal theory of functions and functionals. The - calculus: Connections to higher type recursion theory, proof theory, category theory
Type theory and concurrency
A notation for lambda terms. A generalization of environments
Type checking with universes
A bridge between constructive logic and computer programming
Program development in constructive type theory
Recursive programming with proofs
Characterizing complexity classes by higher type primitive recursive definitions
Constructing type systems over an operational semantics
Coquand's calculus of constructions: A mathematical foundation for a proof development system
Algebraic system specification and development. A survey and annotated bibliography
Verifying programs in the calculus of inductive constructions
Automating the synthesis of decision procedures in a constructive metatheory
Theorem proving in higher order logics. 11th international conference, TPHOLs '98. Canberra, Australia, September 27 - October 1, 1998. Proceedings
Integrating computer algebra into proof planning
A conservative look at operational semantics with variable binding
Representing scope in intuitionistic deductions
From constructivism to computer science
Adaptation of declaratively represented methods in proof planning
Metalogical frameworks. II: Developing a reflected decision procedure
AXIOM
Constructive mathematics: a foundation for computable analysis
Coq
Automated deduction -- CADE-11. Proceedings of the 11th international conference held in Saratoga Springs, NY, USA, June 15--18, 1992
Lazy techniques for fully expansive theorem proving
Implementing tactics and tacticals in a higher-order logic programming language
Computational foundations of basic recursive function theory
Realizability interpretation of coinductive definitions and program synthesis with streams
Defining concurrent processes constructively
Set theory for verification. I: From foundations to functions
IMPS: An interactive mathematical proof system
Isabelle
Constructing specification morphisms
Synthesis of ML programs in the system Coq
\(QPC_ 2\): A constructive calculus with parameterized specifications
Toward formal development of programs from algebraic specifications: Parameterisation revisited
Structured theory presentations and logic representations
Realizability interpretation of generalized inductive definitions
An overview of the Tecton proof system
SETHEO
Proviola
Cubical Agda
Refiner
Proving Ramsey's theory by the cover set induction: A case and comparision study.
Embedding complex decision procedures inside an interactive theorem prover.
Hypersequents, logical consequence and intermediate logics for concurrency
Theorema
TPS
Using tactics to reformulate formulae for resolution theorem proving
Program tactics and logic tactics
Indexed types
APS-1
ML
Reuse of proofs in software verification
AutoBayes/CC
IsaPlanner
PREVAIL
ELAN
OBSCURE
OTTER
ALISA
Automated deduction - CADE-17. 17th international conference, Pittsburgh, PA, USA, June 17--20, 2000. Proceedings
The calculus of constructions as a framework for proof search with set variable instantiation
Search algorithms in type theory
Proof-search in type-theoretic languages: An introduction
Normal natural deduction proofs (in classical logic)
RAISE
Program development schemata as derived rules
OMRS
MAYA
A machine-checked implementation of Buchberger's algorithm
PVS
A taxonomy of parallel strategies for deduction
Autarkic computations in formal proofs
Logic based program synthesis and transformation. 11th international workshop, LOPSTR 2001, Paphos, Cyprus, November 28--30, 2001. Selected papers
Rewriting logic: Roadmap and bibliography
MetaPRL
Mizar
FoCaLiZe and Dedukti to the rescue for proof interoperability
Meaning explanations at higher dimension
IsaWin
TAS
Isabelle/ZF
Miranda
From types to sets by local type definition in higher-order logic
Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
TeXmacs
Incorporating quotation and evaluation into Church's type theory
HOL
Formalizing ring theory in PVS
HOL Light QE
Analogy calculus
Analogical program derivation based on type theory

This page was built for software: Nuprl