Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem (Q3100205): Difference between revisions

@@ 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 @@
+Psi-calculi: a framework for mobile processes with nominal data and logic
+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 @@
+Extending Sledgehammer with SMT Solvers
@@ Property / cites work: Extending Sledgehammer with SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Q4843179
@@ Property / cites work: Q4843179 / 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 @@
+Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
+Normal rank
@@ Property / cites work @@
+Mechanised Computability Theory
@@ Property / cites work: Mechanised Computability Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Nominal logic, a first order theory of names and binding
+Normal rank
@@ Property / cites work @@
+Automated Deduction – CADE-20
@@ Property / cites work: Automated Deduction – CADE-20 / rank @@
+Normal rank
@@ Property / cites work @@
+A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Mechanizing the metatheory of LF
@@ Property / cites work: Mechanizing the metatheory of LF / rank @@
+Normal rank
@@ Property / cites work @@
+General Bindings and Alpha-Equivalence in Nominal Isabelle
+Normal rank