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)

• Intuitionistic completeness of first-order logic
• Twenty years of rewriting logic
• Constructive analysis, types and exact real numbers
• Dependent Types at Work
• Title not available (Why is that?)
• Title not available (Why is that?)
• The future of logic: foundation-independence
• User interaction with the Matita proof assistant
• Program specification and data refinement in type theory
• Unifying sets and programs via dependent types
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Normalizing Intuitionistic Set Theory with Inaccessible Sets
• Towards Knowledge Management for HOL Light
• Do-it-yourself type theory
• Functional and Logic Programming
• Representing model theory in a type-theoretical logical framework
• Rippling: A heuristic for guiding inductive proofs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Mechanical Verification of a Constructive Proof for FLP
• The Twelf Proof Assistant
• Mathematical Knowledge Management
• Logic and program semantics. Essays dedicated to Dexter Kozen on the occasion of his 60th birthday
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theorem proving in higher order logics. 14th international conference, TPHOLs 2001, Edinburgh, Scotland, GB, September 3--6, 2001. Proceedings
• Mechanizing metatheory in a logical framework
• Constructive mathematics: a foundation for computable analysis
• Towards MKM in the large: modular representation and scalable software architecture
• From constructivism to computer science
• A foundational view on integration problems
• Towards logical frameworks in the heterogeneous tool set Hets
• Theorem Proving in Higher Order Logics
• Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection
• Hypersequents, logical consequence and intermediate logics for concurrency
• Knowledge-based synthesis of distributed systems using event structures
• Characterizing complexity classes by higher type primitive recursive definitions
• Types for Proofs and Programs
• Logic and Computation
• Experiments with proof plans for induction
• Primitive recursion for higher-order abstract syntax
• Adding equations to System F types
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Computer supported mathematics with \(\Omega\)MEGA
• Higher-order substitutions
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Automath and Pure Type Systems
• Set theory for verification. I: From foundations to functions
• Embedding complex decision procedures inside an interactive theorem prover.
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Verifying programs in the calculus of inductive constructions
• Integrating computer algebra into proof planning
• Nuprl's class theory and its applications
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Mathematical Knowledge Management
• The automation of proof by mathematical induction
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
• Title not available (Why is that?)
• Logic for Programming, Artificial Intelligence, and Reasoning
• Title not available (Why is that?)
• HOL Light QE
• Title not available (Why is that?)
• Nuprl-Light: An implementation framework for higher-order logics
• TPS: A theorem-proving system for classical type theory
• Mathematical Knowledge Management
• Proofs-as-imperative-programs: application to synthesis of contracts
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formalizing Arrow's theorem
• Representing and Reasoning with Operational Semantics
• TPS: A hybrid automatic-interactive system for developing proofs
• Terminating general recursion
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• The Watson theorem prover
• Title not available (Why is that?)
• Reconstructing proofs at the assertion level
• IMPS: An interactive mathematical proof system
• An overview of the Tecton proof system
• Frontiers of Combining Systems
• Towards a Formally Verified Proof Assistant
• Structured theory presentations and logic representations
• FoCaLiZe and Dedukti to the rescue for proof interoperability
• Fixpoints and search in PVS
• Rewriting logic: Roadmap and bibliography
• Synthesis of ML programs in the system Coq
• Constructing recursion operators in intuitionistic type theory
• Title not available (Why is that?)
• The practice of logical frameworks
• Title not available (Why is that?)
• 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

This page was built for software: Nuprl