Nuprl

swMATH6751WikidataQ22907407 ScholiaQ22907407MaRDI QIDQ18826FDOQ18826

Author name not available (Why is that?)

Described by source

• Nuprl as logical framework for automating proofs in category theory
• Innovations in computational type theory using Nuprl
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication

Cited In (only showing first 100 items - show all)

• Dependent types with subtyping and late-bound overloading
• Structuring metatheory on inductive definitions
• Theorem proving in technology transfer: The user's point of view
• \textsc{PSync}: a partially synchronous language for fault-tolerant distributed algorithms
• From types to sets by local type definition in higher-order logic
• Canonicity for 2-dimensional type theory
• Algebraic methodology and software technology. 5th international conference, AMAST '96, Munich, Germany, July 1-5, 1996. Proceedings
• From types to sets by local type definitions in higher-order logic
• Logic Based Program Synthesis and Transformation
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• Logic based program synthesis and transformation. 11th international workshop, LOPSTR 2001, Paphos, Cyprus, November 28--30, 2001. Selected papers
• Rewriting, inference, and proof
• Reuse of proofs in software verification
• Mechanized metatheory revisited
• Title not available (Why is that?)
• Title not available (Why is that?)
• A dynamic logic for acting, sensing, and planning
• Incorporating quotation and evaluation into Church's type theory
• Trends in trends in functional programming 1999/2000 versus 2007/2008
• Title not available (Why is that?)
• Automated complexity analysis of Nuprl extracted programs
• Title not available (Why is that?)
• Lazy techniques for fully expansive theorem proving
• The calculus of dependent lambda eliminations
• An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
• Title not available (Why is that?)
• \(QPC_ 2\): A constructive calculus with parameterized specifications
• Building Mathematics-Based Software Systems to Advance Science and Create Knowledge
• Formalizing ring theory in PVS
• Constructing specification morphisms
• Title not available (Why is that?)
• Title not available (Why is that?)
• Representing proof transformations for program optimization
• Bar induction is compatible with constructive type theory
• Decidable higher-order unification problems
• Analogical program derivation based on type theory
• Title not available (Why is that?)
• An overview of a formal framework for managing mathematics
• Meaning explanations at higher dimension
• Proving Ramsey's theory by the cover set induction: A case and comparision study.
• Guarded dependent type theory with coinductive types
• Title not available (Why is that?)
• Applicable mathematics in a minimal computational theory of sets
• Title not available (Why is that?)
• Proof-search in type-theoretic languages: An introduction
• The calculus of constructions as a framework for proof search with set variable instantiation
• Program tactics and logic tactics
• Using tactics to reformulate formulae for resolution theorem proving
• Analogy calculus
• Program development schemata as derived rules
• Proof search with set variable instantiation in the calculus of constructions
• The seventeen provers of the world. Foreword by Dana S. Scott..
• Title not available (Why is that?)
• Interpretations of recursively defined types
• Theo: An interactive proof development system
• Insight in discrete geometry and computational content of a discrete model of the continuum
• Building reliable, high-performance networks with the Nuprl proof development system
• Title not available (Why is that?)
• Defining concurrent processes constructively
• Verifying a signature architecture: a comparative case study
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The foundation of a generic theorem prover
• Automated higher-order complexity analysis
• The seven virtues of simple type theory
• Automated deduction -- CADE-11. Proceedings of the 11th international conference held in Saratoga Springs, NY, USA, June 15--18, 1992
• Type theory and concurrency
• Verification conditions are code
• Discovering applications of higher order functions through proof planning
• A conservative look at operational semantics with variable binding
• Typed context awareness ambient calculus for pervasive applications
• Indexed types
• A Ramsey theorem in Boyer-Moore logic
• Exception tracking in an open world
• Logic of subtyping
• Normal natural deduction proofs (in classical logic)
• A notation for lambda terms. A generalization of environments
• Refutation-based synthesis in SMT
• Title not available (Why is that?)
• Classification of alignments between concepts of formal mathematical systems
• Title not available (Why is that?)
• Refinement Types as Proof Irrelevance
• Toward formal development of programs from algebraic specifications: Parameterisation revisited
• Automated deduction - CADE-17. 17th international conference, Pittsburgh, PA, USA, June 17--20, 2000. Proceedings
• Title not available (Why is that?)
• A uniform procedure for converting matrix proofs into sequent-style systems
• Title not available (Why is that?)
• Knowledge-based proof planning
• Search algorithms in type theory
• Artificial Intelligence and Symbolic Computation
• Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm
• Title not available (Why is that?)
• A machine-checked implementation of Buchberger's algorithm
• Autarkic computations in formal proofs
• Towards a computation system based on set theory
• Equivalences between logics and their representing type theories

This page was built for software: Nuprl