Canonical Big Operators (Q3543652): Difference between revisions

@@ Property / describes a project that uses @@
+HOL Light
@@ Property / describes a project that uses: HOL Light / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / 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.1007/978-3-540-71067-7_11
+Normal rank
@@ Property / OpenAlex ID @@
+W1542112699
@@ Property / OpenAlex ID: W1542112699 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof-irrelevance out of excluded-middle and choice in the calculus of constructions
+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 @@
+Q3075246
@@ Property / cites work: Q3075246 / rank @@
+Normal rank
@@ Property / cites work @@
+A Modular Formalisation of Finite Group Theory
@@ Property / cites work: A Modular Formalisation of Finite Group Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Organizing numerical theories using axiomatic type classes
+Normal rank
@@ Property / cites work @@
+Q2754063
@@ Property / cites work: Q2754063 / rank @@
+Normal rank