Innovations in computational type theory using Nuprl (Q865639): Difference between revisions

@@ Property / author @@
-Mark Bickford
@@ Property / author: Mark Bickford / rank @@
-Normal rank
@@ Property / author @@
-Robert L. Constable
@@ Property / author: Robert L. Constable / rank @@
-Normal rank
@@ Property / author @@
-Christoph Kreitz
@@ Property / author: Christoph Kreitz / rank @@
-Normal rank
@@ Property / author @@
+Mark Bickford
@@ Property / author: Mark Bickford / rank @@
+Normal rank
@@ Property / author @@
+Robert L. Constable
@@ Property / author: Robert L. Constable / rank @@
+Normal rank
@@ Property / author @@
+Christoph Kreitz
@@ Property / author: Christoph Kreitz / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PVS
@@ Property / describes a project that uses: PVS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MetaPRL
@@ Property / describes a project that uses: MetaPRL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Automath
@@ Property / describes a project that uses: Automath / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LCF
@@ Property / describes a project that uses: LCF / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Horus
@@ Property / describes a project that uses: Horus / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OMDoc
@@ Property / describes a project that uses: OMDoc / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+JProver
@@ Property / describes a project that uses: JProver / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MathWeb
@@ Property / describes a project that uses: MathWeb / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.jal.2005.10.005
+Normal rank
@@ Property / OpenAlex ID @@
+W1977189131
@@ Property / OpenAlex ID: W1977189131 / rank @@
+Normal rank
@@ Property / Wikidata QID @@
+Q56228326
@@ Property / Wikidata QID: Q56228326 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2723417
@@ Property / cites work: Q2723417 / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematical knowledge management in HELM
@@ Property / cites work: Mathematical knowledge management in HELM / rank @@
+Normal rank
@@ Property / cites work @@
+Q3823124
@@ Property / cites work: Q3823124 / rank @@
+Normal rank
@@ Property / cites work @@
+Emergence of Scaling in Random Networks
@@ Property / cites work: Emergence of Scaling in Random Networks / rank @@
+Normal rank
@@ Property / cites work @@
+Q4023900
@@ Property / cites work: Q4023900 / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Q4247299
@@ Property / cites work: Q4247299 / rank @@
+Normal rank
@@ Property / cites work @@
+Intuitionistic completeness of first-order logic
@@ Property / cites work: Intuitionistic completeness of first-order logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q4790655
@@ Property / cites work: Q4790655 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5573965
@@ Property / cites work: Q5573965 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5565097
@@ Property / cites work: Q5565097 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3894958
@@ Property / cites work: Q3894958 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3235339
@@ Property / cites work: Q3235339 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5670174
@@ Property / cites work: Q5670174 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3687706
@@ Property / cites work: Q3687706 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4215639
@@ Property / cites work: Q4215639 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2752048
@@ Property / cites work: Q2752048 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3484381
@@ Property / cites work: Q3484381 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4513619
@@ Property / cites work: Q4513619 / rank @@
+Normal rank
@@ Property / cites work @@
+An introduction to the PL/CV2 programming logic
@@ Property / cites work: An introduction to the PL/CV2 programming logic / rank @@
+Normal rank
@@ Property / cites work @@
+Writing programs that construct proofs
@@ Property / cites work: Writing programs that construct proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Q3875311
@@ Property / cites work: Q3875311 / rank @@
+Normal rank
@@ Property / cites work @@
+The Type Theory of PL/CV3
@@ Property / cites work: The Type Theory of PL/CV3 / rank @@
+Normal rank
@@ Property / cites work @@
+Foundations for the implementation of higher-order subtyping
+Normal rank
@@ Property / cites work @@
+Combinatory logic. With two sections by William Craig.
+Normal rank
@@ Property / cites work @@
+Q5610115
@@ Property / cites work: Q5610115 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4012883
@@ Property / cites work: Q4012883 / rank @@
+Normal rank
@@ Property / cites work @@
+Hybrid interactive theorem proving using nuprl and HOL
+Normal rank
@@ Property / cites work @@
+Q3994895
@@ Property / cites work: Q3994895 / rank @@
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem proving in higher order logics. 16th international conference, TPHOLs 2003, Rome, Italy, September 8--12, 2003. Proceedings
+Normal rank
@@ Property / cites work @@
+Q3204055
@@ Property / cites work: Q3204055 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4375633
@@ Property / cites work: Q4375633 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2782486
@@ Property / cites work: Q2782486 / rank @@
+Normal rank
@@ Property / cites work @@
+Exploring abstract algebra in constructive type theory
+Normal rank
@@ Property / cites work @@
+Q5812175
@@ Property / cites work: Q5812175 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4250236
@@ Property / cites work: Q4250236 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4471938
@@ Property / cites work: Q4471938 / rank @@
+Normal rank
@@ Property / cites work @@
+Building reliable, high-performance networks with the Nuprl proof development system
+Normal rank
@@ Property / cites work @@
+Q4520768
@@ Property / cites work: Q4520768 / rank @@
+Normal rank
@@ Property / cites work @@
+A uniform procedure for converting matrix proofs into sequent-style systems
+Normal rank
@@ Property / cites work @@
+Time, clocks, and the ordering of events in a distributed system
+Normal rank
@@ Property / cites work @@
+The mutual exclusion problem
@@ Property / cites work: The mutual exclusion problem / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematical Knowledge Management
@@ Property / cites work: Mathematical Knowledge Management / rank @@
+Normal rank
@@ Property / cites work @@
+Q3126969
@@ Property / cites work: Q3126969 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4099613
@@ Property / cites work: Q4099613 / rank @@
+Normal rank
@@ Property / cites work @@
+Constructive mathematics and computer programming
@@ Property / cites work: Constructive mathematics and computer programming / rank @@
+Normal rank
@@ Property / cites work @@
+Q3688389
@@ Property / cites work: Q3688389 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999206
@@ Property / cites work: Q3999206 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999860
@@ Property / cites work: Q3999860 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754063
@@ Property / cites work: Q2754063 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4539627
@@ Property / cites work: Q4539627 / rank @@
+Normal rank
@@ Property / cites work @@
+Data Types as Lattices
@@ Property / cites work: Data Types as Lattices / rank @@
+Normal rank
@@ Property / cites work @@
+Q5560258
@@ Property / cites work: Q5560258 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4003339
@@ Property / cites work: Q4003339 / rank @@
+Normal rank
@@ Property / cites work @@
+Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
+Normal rank
@@ Property / cites work @@
+Constructivism in mathematics. An introduction. Volume II
+Normal rank
@@ Property / cites work @@
+Q4809049
@@ Property / cites work: Q4809049 / rank @@
+Normal rank