General Bindings and Alpha-Equivalence in Nominal Isabelle (Q5892493): Difference between revisions

@@ Property / OpenAlex ID @@
+W1495561703
@@ Property / OpenAlex ID: W1495561703 / rank @@
+Normal rank
@@ Property / arXiv ID @@
+.0136
@@ Property / arXiv ID: 1206.0136 / rank @@
+Normal rank
@@ Property / cites work @@
+ΠΣ: Dependent Types without the Sugar
@@ Property / cites work: ΠΣ: Dependent Types without the Sugar / rank @@
+Normal rank
@@ Property / cites work @@
+Psi-calculi in Isabelle
@@ Property / cites work: Psi-calculi in Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+The locally nameless representation
@@ Property / cites work: The locally nameless representation / rank @@
+Normal rank
@@ Property / cites work @@
+Scrap your nameplate
@@ Property / cites work: Scrap your nameplate / 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 @@
+A New Foundation for Nominal Isabelle
@@ Property / cites work: A New Foundation for Nominal Isabelle / rank @@
+Normal rank
@@ Property / cites work @@
+General Bindings and Alpha-Equivalence in Nominal Isabelle
+Normal rank
@@ Property / cites work @@
+Towards a mechanized metatheory of standard ML
@@ Property / cites work: Towards a mechanized metatheory of standard ML / rank @@
+Normal rank
@@ Property / cites work @@
+Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
+Normal rank
@@ Property / cites work @@
+Nominal logic, a first order theory of names and binding
+Normal rank
@@ Property / cites work @@
+External and internal syntax of the \(\lambda \)-calculus
+Normal rank
@@ Property / cites work @@
+Ott: Effective tool support for the working semanticist
+Normal rank
@@ Property / cites work @@
+The design and implementation of typed scheme
@@ Property / cites work: The design and implementation of typed scheme / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanizing the metatheory of LF
@@ Property / cites work: Mechanizing the metatheory of LF / rank @@
+Normal rank
@@ Property / cites work @@
+Q3400637
@@ Property / cites work: Q3400637 / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
+Normal rank