Lax Theory Morphisms (Q5277906): Difference between revisions

@@ Property / describes a project that uses @@
+QMT
@@ Property / describes a project that uses: QMT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+LATIN
@@ Property / describes a project that uses: LATIN / 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.1145/2818644
@@ Property / full work available at URL: https://doi.org/10.1145/2818644 / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2095327196
@@ Property / OpenAlex ID: W2095327196 / rank @@
+Normal rank
@@ Property / cites work @@
+Proofs for free
@@ Property / cites work: Proofs for free / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanizing the Metatheory of Sledgehammer
@@ Property / cites work: Mechanizing the Metatheory of Sledgehammer / rank @@
+Normal rank
@@ Property / cites work @@
+Project Abstract: Logic Atlas and Integrator (LATIN)
+Normal rank
@@ Property / cites work @@
+Combinatory logic. With two sections by William Craig.
+Normal rank
@@ Property / cites work @@
+Q4052071
@@ Property / cites work: Q4052071 / 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 @@
+Institutions: abstract model theory for specification and programming
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+Structured theory presentations and logic representations
+Normal rank
@@ Property / cites work @@
+Representing model theory in a type-theoretical logical framework
+Normal rank
@@ Property / cites work @@
+Isabelle. A generic theorem prover
@@ Property / cites work: Isabelle. A generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754136
@@ Property / cites work: Q2754136 / rank @@
+Normal rank
@@ Property / cites work @@
+A logical framework combining model and proof theory
+Normal rank
@@ Property / cites work @@
+The MMT API: A Generic MKM System
@@ Property / cites work: The MMT API: A Generic MKM System / rank @@
+Normal rank
@@ Property / cites work @@
+How to identify, translate and combine logics?
@@ Property / cites work: How to identify, translate and combine logics? / rank @@
+Normal rank
@@ Property / cites work @@
+A scalable module system
@@ Property / cites work: A scalable module system / rank @@
+Normal rank
@@ Property / cites work @@
+Logical relations for a logical framework
@@ Property / cites work: Logical relations for a logical framework / rank @@
+Normal rank
@@ Property / cites work @@
+Q3666260
@@ Property / cites work: Q3666260 / rank @@
+Normal rank
@@ Property / cites work @@
+An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf
+Normal rank