Nominal techniques in Isabelle/HOL (Q928672): Difference between revisions

@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PoplMark
@@ Property / describes a project that uses: PoplMark / 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/s10817-008-9097-2
+Normal rank
@@ Property / OpenAlex ID @@
+W2037026294
@@ Property / OpenAlex ID: W2037026294 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4484329
@@ Property / cites work: Q4484329 / rank @@
+Normal rank
@@ Property / cites work @@
+Engineering formal metatheory
@@ Property / cites work: Engineering formal metatheory / 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 @@
+The lambda calculus, its syntax and semantics
@@ Property / cites work: The lambda calculus, its syntax and semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Formalising the π-Calculus Using Nominal Logic
@@ Property / cites work: Formalising the π-Calculus Using Nominal Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q3024831
@@ Property / cites work: Q3024831 / rank @@
+Normal rank
@@ Property / cites work @@
+Higher order unification via explicit substitutions
+Normal rank
@@ Property / cites work @@
+A new approach to abstract syntax with variable binding
+Normal rank
@@ Property / cites work @@
+Q3994895
@@ Property / cites work: Q3994895 / 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 @@
+Disjunction and existence under implication in elementary intuitionistic formalisms
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+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 @@
+Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
+Normal rank
@@ Property / cites work @@
+Nominal logic, a first order theory of names and binding
+Normal rank
@@ Property / cites work @@
+Alpha-structural recursion and induction
@@ Property / cites work: Alpha-structural recursion and induction / rank @@
+Normal rank
@@ Property / cites work @@
+Q2723408
@@ Property / cites work: Q2723408 / rank @@
+Normal rank
@@ Property / cites work @@
+Parallel reductions in \(\lambda\)-calculus
@@ Property / cites work: Parallel reductions in \(\lambda\)-calculus / rank @@
+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 @@
+A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Barendregt’s Variable Convention in Rule Inductions
+Normal rank
@@ Property / cites work @@
+Nominal unification
@@ Property / cites work: Nominal unification / rank @@
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+Structured Induction Proofs in Isabelle/Isar
@@ Property / cites work: Structured Induction Proofs in Isabelle/Isar / rank @@
+Normal rank