The seven virtues of simple type theory (Q946569): Difference between revisions

@@ Property / describes a project that uses @@
+TPS
@@ Property / describes a project that uses: TPS / 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 @@
+ETPS
@@ Property / describes a project that uses: ETPS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ML
@@ Property / describes a project that uses: ML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+IMPS
@@ Property / describes a project that uses: IMPS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Z
@@ Property / describes a project that uses: Z / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Nuprl
@@ Property / describes a project that uses: Nuprl / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LEGO
@@ Property / describes a project that uses: LEGO / 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.2007.11.001
+Normal rank
@@ Property / OpenAlex ID @@
+W2097181978
@@ Property / OpenAlex ID: W2097181978 / rank @@
+Normal rank
@@ Property / cites work @@
+The B-Book
@@ Property / cites work: The B-Book / rank @@
+Normal rank
@@ Property / cites work @@
+A reduction of the axioms for the theory of prepositional types
+Normal rank
@@ Property / cites work @@
+An introduction to mathematical logic and type theory: To truth through proof.
+Normal rank
@@ Property / cites work @@
+TPS: A theorem-proving system for classical type theory
+Normal rank
@@ Property / cites work @@
+The calculus of constructions
@@ Property / cites work: The calculus of constructions / rank @@
+Normal rank
@@ Property / cites work @@
+A partial functions version of Church's simple theory of types
+Normal rank
@@ Property / cites work @@
+A simple type theory with partial functions and subtypes
+Normal rank
@@ Property / cites work @@
+Automated Reasoning
@@ Property / cites work: Automated Reasoning / rank @@
+Normal rank
@@ Property / cites work @@
+IMPS: An interactive mathematical proof system
@@ Property / cites work: IMPS: An interactive mathematical proof system / rank @@
+Normal rank
@@ Property / cites work @@
+Q4674788
@@ Property / cites work: Q4674788 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3875893
@@ Property / cites work: Q3875893 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3994895
@@ Property / cites work: Q3994895 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / 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 @@
+Q4342091
@@ Property / cites work: Q4342091 / rank @@
+Normal rank
@@ Property / cites work @@
+The completeness of the first-order functional calculus
+Normal rank
@@ Property / cites work @@
+Completeness in the theory of types
@@ Property / cites work: Completeness in the theory of types / rank @@
+Normal rank
@@ Property / cites work @@
+A theory of prepositional types
@@ Property / cites work: A theory of prepositional types / rank @@
+Normal rank
@@ Property / cites work @@
+The Discovery of My Completeness Proofs
@@ Property / cites work: The Discovery of My Completeness Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Q4281475
@@ Property / cites work: Q4281475 / rank @@
+Normal rank
@@ Property / cites work @@
+On the consistency of a slight (?) modification of Quine's 'New Foundations'
+Normal rank
@@ Property / cites work @@
+Q4012178
@@ Property / cites work: Q4012178 / rank @@
+Normal rank
@@ Property / cites work @@
+A mechanization of strong Kleene logic for partial functions
+Normal rank
@@ Property / cites work @@
+Q3727946
@@ Property / cites work: Q3727946 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4692751
@@ Property / cites work: Q4692751 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3688389
@@ Property / cites work: Q3688389 / rank @@
+Normal rank
@@ Property / cites work @@
+The strength of Mac Lane set theory
@@ Property / cites work: The strength of Mac Lane set theory / rank @@
+Normal rank
@@ Property / cites work @@
+Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
+Normal rank
@@ Property / cites work @@
+Isabelle. A generic theorem prover
@@ Property / cites work: Isabelle. A generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Q3995087
@@ Property / cites work: Q3995087 / rank @@
+Normal rank
@@ Property / cites work @@
+Practical forms of type theory
@@ Property / cites work: Practical forms of type theory / rank @@
+Normal rank