Nuprl
From MaRDI portal
Software:18826
swMATH6751WikidataQ22907407 ScholiaQ22907407MaRDI QIDQ18826FDOQ18826
Author name not available (Why is that?)
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
- Guarded Dependent Type Theory with Coinductive Types
- \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
- 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
- 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
- Bar Induction is Compatible with Constructive Type Theory
- Trends in trends in functional programming 1999/2000 versus 2007/2008
- From Types to Sets by Local Type Definitions in Higher-Order Logic
- Applicable Mathematics in a Minimal Computational Theory of Sets
- 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?)
- Proof search with set variable instantiation in the Calculus of Constructions
- \(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
- 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.
- Rewriting, Inference, and Proof
- Title not available (Why is that?)
- 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
- Title not available (Why is that?)
- Optimization techniques for propositional intuitionistic logic and their implementation
- Title not available (Why is that?)
- An approach to automatic deductive synthesis of functional programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Types for Proofs and Programs
- Exploring abstract algebra in constructive type theory
- Hybrid interactive theorem proving using nuprl and HOL
- Mathematical Knowledge Management
- 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
- KI 2004: Advances in Artificial Intelligence
- A framework for defining logical frameworks
- Mechanizing Mathematical Reasoning
- Representing scope in intuitionistic deductions
- Adaptation of declaratively represented methods in proof planning
- Title not available (Why is that?)
- Automated Reasoning with Analytic Tableaux and Related Methods
- Automated Reasoning with Analytic Tableaux and Related Methods
- Constructing type systems over an operational semantics
- Choices in representation and reduction strategies for lambda terms in intensional contexts
- A proof-centric approach to mathematical assistants
- Supporting the formal verification of mathematical texts
- Metalogical frameworks. II: Developing a reflected decision procedure
- The Girard-Reynolds isomorphism (second edition)
- Theorem Proving in Higher Order Logics
- Title not available (Why is that?)
- An Interpretation of Isabelle/HOL in HOL Light
- Type checking with universes
- A bridge between constructive logic and computer programming
- Title not available (Why is that?)
- Title not available (Why is that?)
- The Girard-Reynolds isomorphism
- Title not available (Why is that?)
- Title not available (Why is that?)
- Proof assistants: history, ideas and future
- Realizability interpretation of generalized inductive definitions
- Propositional functions and families of types
- Program derivation in type theory: A partitioning problem
- Realizability interpretation of coinductive definitions and program synthesis with streams
- On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
- Program development in constructive type theory
- Recursive programming with proofs
- Dependent types for program termination verification
- Title not available (Why is that?)
- The Implicit Calculus of Constructions as a Programming Language with Dependent Types
- Coquand's calculus of constructions: A mathematical foundation for a proof development system
- Algebraic system specification and development. A survey and annotated bibliography
This page was built for software: Nuprl
