Mechanizing metatheory in a logical framework (Q5308093): Difference between revisions

@@ Property / cites work @@
+On equivalence and canonical forms in the LF type theory
+Normal rank
@@ Property / cites work @@
+A Representation of Fω in LF
@@ Property / cites work: A Representation of Fω in LF / rank @@
+Normal rank
@@ Property / cites work @@
+Dependent types ensure partial correctness of theorem provers
+Normal rank
@@ Property / cites work @@
+A framework for defining logics
@@ Property / cites work: A framework for defining logics / rank @@
+Normal rank
@@ Property / cites work @@
+A linear logical framework
@@ Property / cites work: A linear logical framework / rank @@
+Normal rank