Nuprl

swMATH6751WikidataQ22907407MaRDI QIDQ18826

No author found.

Described by source

• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Innovations in computational type theory using Nuprl
• Nuprl as Logical Framework for Automating Proofs in Category Theory

Related Items (only showing first 100 items - show all)

Structured theory presentations and logic representations ⋮ The seventeen provers of the world. Foreword by Dana S. Scott.. ⋮ 8th international conference on automated deduction, Oxford, England, July 27 -- August 1, 1986. Proceedings ⋮ Realizability interpretation of generalized inductive definitions ⋮ Insight in discrete geometry and computational content of a discrete model of the continuum ⋮ An overview of the Tecton proof system ⋮ Constructing recursion operators in intuitionistic type theory ⋮ On the syntax of Martin-Löf's type theories ⋮ 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 ⋮ Verification conditions are code ⋮ Choices in representation and reduction strategies for lambda terms in intensional contexts ⋮ Terminating general recursion ⋮ TPS: A hybrid automatic-interactive system for developing proofs ⋮ \textit{Theorema}: Towards computer-aided mathematical theory exploration ⋮ A proof-centric approach to mathematical assistants ⋮ Computer supported mathematics with \(\Omega\)MEGA ⋮ Supporting the formal verification of mathematical texts ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ Verifying a signature architecture: a comparative case study ⋮ Using tactics to reformulate formulae for resolution theorem proving ⋮ Program tactics and logic tactics ⋮ Type theory and concurrency ⋮ The Girard-Reynolds isomorphism (second edition) ⋮ A notation for lambda terms. A generalization of environments ⋮ Intuitionistic completeness of first-order logic ⋮ Indexed types ⋮ Unifying sets and programs via dependent types ⋮ Logic and program semantics. Essays dedicated to Dexter Kozen on the occasion of his 60th birthday ⋮ Typed context awareness ambient calculus for pervasive applications ⋮ Extracting the resolution algorithm from a completeness proof for the propositional calculus ⋮ Propositional functions and families of types ⋮ Coalgebras in functional programming and type theory ⋮ Do-it-yourself type theory ⋮ Proofs and programs: A naïve approach to program extraction ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ Reuse of proofs in software verification ⋮ Representing model theory in a type-theoretical logical framework ⋮ A knowledge-based analysis of global function computation ⋮ Type checking with universes ⋮ A bridge between constructive logic and computer programming ⋮ The seven virtues of simple type theory ⋮ Program development in constructive type theory ⋮ Recursive programming with proofs ⋮ Characterizing complexity classes by higher type primitive recursive definitions ⋮ Interpretations of recursively defined types ⋮ Rippling: A heuristic for guiding inductive proofs ⋮ Constructing type systems over an operational semantics ⋮ Coquand's calculus of constructions: A mathematical foundation for a proof development system ⋮ Using typed lambda calculus to implement formal systems on a machine ⋮ Theo: An interactive proof development system ⋮ On specifications, subset types and interpretation of proposition in type theory ⋮ Optimization techniques for propositional intuitionistic logic and their implementation ⋮ Algebraic system specification and development. A survey and annotated bibliography ⋮ Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. ⋮ Exception tracking in an open world ⋮ All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM. ⋮ Verifying programs in the calculus of inductive constructions ⋮ Automating the synthesis of decision procedures in a constructive metatheory ⋮ Functorial polymorphism ⋮ Theorem proving in higher order logics. 11th international conference, TPHOLs '98. Canberra, Australia, September 27 - October 1, 1998. Proceedings ⋮ Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm ⋮ 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 ⋮ Automated deduction - CADE-17. 17th international conference, Pittsburgh, PA, USA, June 17--20, 2000. Proceedings ⋮ Metalogical frameworks. II: Developing a reflected decision procedure ⋮ Proof assistants: history, ideas and future ⋮ Formalizing Arrow's theorem ⋮ 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) ⋮ Constructive mathematics: a foundation for computable analysis ⋮ Continuity and Lipschitz constants for projections ⋮ Program development schemata as derived rules ⋮ 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 ⋮ A machine-checked implementation of Buchberger's algorithm ⋮ 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 ⋮ A taxonomy of parallel strategies for deduction ⋮ Extraction of redundancy-free programs from constructive natural deduction proofs ⋮ Experiments with proof plans for induction ⋮ Set theory for verification. I: From foundations to functions ⋮ IMPS: An interactive mathematical proof system ⋮ 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 ⋮ Autarkic computations in formal proofs ⋮ A complete mechanization of correctness of a string-preprocessing algorithm ⋮ Logic based program synthesis and transformation. 11th international workshop, LOPSTR 2001, Paphos, Cyprus, November 28--30, 2001. Selected papers ⋮ On modal logics of partial recursive functions ⋮ The future of logic: foundation-independence

This page was built for software: Nuprl