The following pages link to Nuprl (Q18826):
Displaying 50 items.
- The future of logic: foundation-independence (Q263104) (← links)
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- Unifying sets and programs via dependent types (Q408534) (← links)
- Logic and program semantics. Essays dedicated to Dexter Kozen on the occasion of his 60th birthday (Q424407) (← links)
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control (Q444460) (← links)
- Extracting the resolution algorithm from a completeness proof for the propositional calculus (Q636273) (← links)
- Coalgebras in functional programming and type theory (Q639643) (← links)
- Representing model theory in a type-theoretical logical framework (Q654913) (← links)
- A knowledge-based analysis of global function computation (Q660991) (← links)
- Interpretations of recursively defined types (Q685350) (← links)
- Rippling: A heuristic for guiding inductive proofs (Q685548) (← links)
- Using typed lambda calculus to implement formal systems on a machine (Q688571) (← links)
- Theo: An interactive proof development system (Q688727) (← links)
- On specifications, subset types and interpretation of proposition in type theory (Q688736) (← links)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. (Q703860) (← links)
- Exception tracking in an open world (Q724930) (← links)
- Functorial polymorphism (Q753948) (← links)
- Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm (Q757074) (← links)
- Extraction of redundancy-free programs from constructive natural deduction proofs (Q808284) (← links)
- Experiments with proof plans for induction (Q809617) (← links)
- A complete mechanization of correctness of a string-preprocessing algorithm (Q816208) (← links)
- On modal logics of partial recursive functions (Q817692) (← links)
- The seventeen provers of the world. Foreword by Dana S. Scott.. (Q819987) (← links)
- Insight in discrete geometry and computational content of a discrete model of the continuum (Q834257) (← links)
- Verification conditions are code (Q855274) (← links)
- Choices in representation and reduction strategies for lambda terms in intensional contexts (Q861365) (← links)
- TPS: A hybrid automatic-interactive system for developing proofs (Q865629) (← links)
- \textit{Theorema}: Towards computer-aided mathematical theory exploration (Q865646) (← links)
- A proof-centric approach to mathematical assistants (Q865648) (← links)
- Computer supported mathematics with \(\Omega\)MEGA (Q865650) (← links)
- Supporting the formal verification of mathematical texts (Q865656) (← links)
- Verifying a signature architecture: a comparative case study (Q877156) (← links)
- The Girard-Reynolds isomorphism (second edition) (Q879366) (← links)
- Typed context awareness ambient calculus for pervasive applications (Q903500) (← links)
- Propositional functions and families of types (Q908912) (← links)
- Do-it-yourself type theory (Q911744) (← links)
- Proofs and programs: A naïve approach to program extraction (Q912594) (← links)
- The seven virtues of simple type theory (Q946569) (← links)
- Optimization techniques for propositional intuitionistic logic and their implementation (Q959821) (← links)
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM. (Q997833) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- Formalizing Arrow's theorem (Q1040010) (← links)
- Continuity and Lipschitz constants for projections (Q1044668) (← links)
- 8th international conference on automated deduction, Oxford, England, July 27 -- August 1, 1986. Proceedings (Q1079552) (← links)
- Constructing recursion operators in intuitionistic type theory (Q1094421) (← links)
- On the syntax of Martin-Löf's type theories (Q1099173) (← links)
- Terminating general recursion (Q1112584) (← links)
- On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory (Q1120558) (← links)
- Type theory and concurrency (Q1124322) (← links)
- A notation for lambda terms. A generalization of environments (Q1129257) (← links)
