Nuprl - MaRDI portal

Cited in

(only showing first 100 items - show all)

Functorial polymorphism
Intuitionistic completeness of first-order logic
The practice of logical frameworks
The seventeen provers of the world. Foreword by Dana S. Scott..
Proof search with set variable instantiation in the calculus of constructions
A First Look into a Formal and Constructive Approach for Discrete Geometry Using Nonstandard Analysis
scientific article; zbMATH DE number 512790 (Why is no real title available?)
Dependent types with subtyping and late-bound overloading
Structuring metatheory on inductive definitions
Theorem proving in technology transfer: The user's point of view
scientific article; zbMATH DE number 1348467 (Why is no real title available?)
Twenty years of rewriting logic
\textsc{PSync}: a partially synchronous language for fault-tolerant distributed algorithms
scientific article; zbMATH DE number 2085176 (Why is no real title available?)
Interpretations of recursively defined types
scientific article; zbMATH DE number 177847 (Why is no real title available?)
Theo: An interactive proof development system
From types to sets by local type definition in higher-order logic
The future of logic: foundation-independence
scientific article; zbMATH DE number 785045 (Why is no real title available?)
Optimization techniques for propositional intuitionistic logic and their implementation
Algebraic methodology and software technology. 5th international conference, AMAST '96, Munich, Germany, July 1-5, 1996. Proceedings
\textsc{Prawf}: an interactive proof system for program extraction
Canonicity for 2-dimensional type theory
Insight in discrete geometry and computational content of a discrete model of the continuum
Constructive analysis, types and exact real numbers
A realizability interpretation of Church's simple theory of types
User interaction with the Matita proof assistant
scientific article; zbMATH DE number 1070622 (Why is no real title available?)
scientific article; zbMATH DE number 1479608 (Why is no real title available?)
scientific article; zbMATH DE number 3986665 (Why is no real title available?)
Dependent Types at Work
An approach to automatic deductive synthesis of functional programs
scientific article; zbMATH DE number 1576852 (Why is no real title available?)
From types to sets by local type definitions in higher-order logic
Program specification and data refinement in type theory
scientific article; zbMATH DE number 29052 (Why is no real title available?)
Unifying sets and programs via dependent types
Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
Building reliable, high-performance networks with the Nuprl proof development system
scientific article; zbMATH DE number 1765685 (Why is no real title available?)
Logic Based Program Synthesis and Transformation
Defining concurrent processes constructively
Do-it-yourself type theory
scientific article; zbMATH DE number 4134038 (Why is no real title available?)
scientific article; zbMATH DE number 2084367 (Why is no real title available?)
Verifying a signature architecture: a comparative case study
A Normalizing Intuitionistic Set Theory with Inaccessible Sets
Towards Knowledge Management for HOL Light
Bar induction. The good, the bad, and the ugly
Computability beyond Church-Turing via choice sequences
Logic based program synthesis and transformation. 11th international workshop, LOPSTR 2001, Paphos, Cyprus, November 28--30, 2001. Selected papers
Representing model theory in a type-theoretical logical framework
scientific article; zbMATH DE number 38948 (Why is no real title available?)
scientific article; zbMATH DE number 4047195 (Why is no real title available?)
scientific article; zbMATH DE number 218497 (Why is no real title available?)
scientific article; zbMATH DE number 1301736 (Why is no real title available?)
Rippling: A heuristic for guiding inductive proofs
Functional and Logic Programming
Manifest Fields and Module Mechanisms in Intensional Type Theory
Theorem Proving in Higher Order Logics
The foundation of a generic theorem prover
Automated higher-order complexity analysis
Twenty Years of Theorem Proving for HOLs Past, Present and Future
Formally computing with the non-computable
scientific article; zbMATH DE number 1332647 (Why is no real title available?)
scientific article; zbMATH DE number 1113859 (Why is no real title available?)
scientific article; zbMATH DE number 1980938 (Why is no real title available?)
The seven virtues of simple type theory
scientific article; zbMATH DE number 1863374 (Why is no real title available?)
scientific article; zbMATH DE number 1863380 (Why is no real title available?)
scientific article; zbMATH DE number 2090073 (Why is no real title available?)
Types for Proofs and Programs
scientific article; zbMATH DE number 4101139 (Why is no real title available?)
Automated deduction -- CADE-11. Proceedings of the 11th international conference held in Saratoga Springs, NY, USA, June 15--18, 1992
Dependently Typed Programming Based on Automated Theorem Proving
scientific article; zbMATH DE number 65530 (Why is no real title available?)
Type theory and concurrency
Exploring abstract algebra in constructive type theory
Rewriting, inference, and proof
scientific article; zbMATH DE number 47007 (Why is no real title available?)
Automating the synthesis of decision procedures in a constructive metatheory
Mechanical Verification of a Constructive Proof for FLP
Theorem proving in higher order logics. 11th international conference, TPHOLs '98. Canberra, Australia, September 27 - October 1, 1998. Proceedings
scientific article; zbMATH DE number 1005001 (Why is no real title available?)
scientific article; zbMATH DE number 1543301 (Why is no real title available?)
scientific article; zbMATH DE number 591911 (Why is no real title available?)
First order logic with domain conditions
Analogy in automated deduction: a survey
The automation of proof: a historical and sociological exploration
Reuse of proofs in software verification
Mathematical Knowledge Management
Algebraic Methodology and Software Technology
The Twelf Proof Assistant
Social processes, program verification and all that
Mechanized metatheory revisited
Generation and presentation of formal mathematical documents
scientific article; zbMATH DE number 53709 (Why is no real title available?)
Logic and program semantics. Essays dedicated to Dexter Kozen on the occasion of his 60th birthday
scientific article; zbMATH DE number 5872266 (Why is no real title available?)

This page was built for software: Nuprl