A list-machine benchmark for mechanized metatheory (Q1945921): Difference between revisions

@@ Property / OpenAlex ID @@
+W2088975898
@@ Property / OpenAlex ID: W2088975898 / rank @@
+Normal rank
@@ Property / cites work @@
+A very modal model of a modern, major, general type system
+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 @@
+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 @@
+Extracting Purely Functional Contents from Logical Inductive Types
+Normal rank
@@ Property / cites work @@
+Coinductive big-step operational semantics
@@ Property / cites work: Coinductive big-step operational semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Stack-based typed assembly language
@@ Property / cites work: Stack-based typed assembly language / rank @@
+Normal rank
@@ Property / cites work @@
+A syntactic approach to type soundness
@@ Property / cites work: A syntactic approach to type soundness / rank @@
+Normal rank