Term-generic logic (Q2339466): Difference between revisions

@@ Property / cites work @@
+Q3912779
@@ Property / cites work: Q3912779 / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Using typed lambda calculus to implement formal systems on a machine
+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 @@
+Engineering formal metatheory
@@ Property / cites work: Engineering formal metatheory / rank @@
+Normal rank
@@ Property / cites work @@
+Q3342534
@@ Property / cites work: Q3342534 / rank @@
+Normal rank
@@ Property / cites work @@
+The semantics of second-order lambda calculus
@@ Property / cites work: The semantics of second-order lambda calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Q5667469
@@ Property / cites work: Q5667469 / rank @@
+Normal rank
@@ Property / cites work @@
+Completeness and Herbrand theorems for nominal logic
+Normal rank
@@ Property / cites work @@
+Q4428296
@@ Property / cites work: Q4428296 / rank @@
+Normal rank
@@ Property / cites work @@
+Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
+Normal rank
@@ Property / cites work @@
+Nominal Algebra and the HSP Theorem
@@ Property / cites work: Nominal Algebra and the HSP Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+A two-level logic approach to reasoning about computations
+Normal rank
@@ Property / cites work @@
+Q3743300
@@ Property / cites work: Q3743300 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5625124
@@ Property / cites work: Q5625124 / rank @@
+Normal rank
@@ Property / cites work @@
+Linear logic
@@ Property / cites work: Linear logic / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanizing metatheory in a logical framework
@@ Property / cites work: Mechanizing metatheory in a logical framework / rank @@
+Normal rank
@@ Property / cites work @@
+Lambda‐Calculus Models and Extensionality
@@ Property / cites work: Lambda‐Calculus Models and Extensionality / rank @@
+Normal rank
@@ Property / cites work @@
+Q4274979
@@ Property / cites work: Q4274979 / rank @@
+Normal rank
@@ Property / cites work @@
+Reasoning with higher-order abstract syntax in a logical framework
+Normal rank
@@ Property / cites work @@
+A calculus of mobile processes. II
@@ Property / cites work: A calculus of mobile processes. II / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+The foundation of a generic theorem prover
@@ Property / cites work: The foundation of a generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
+Normal rank
@@ Property / cites work @@
+Q5714442
@@ Property / cites work: Q5714442 / rank @@
+Normal rank
@@ Property / cites work @@
+A canonical locally named representation of binding
+Normal rank
@@ Property / cites work @@
+Recursion principles for syntax with bindings and substitution
+Normal rank
@@ Property / cites work @@
+Term-Generic Logic
@@ Property / cites work: Term-Generic Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q4068054
@@ Property / cites work: Q4068054 / rank @@
+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 @@
+Logical relations and the typed λ-calculus
@@ Property / cites work: Logical relations and the typed λ-calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Substitution revisited
@@ Property / cites work: Substitution revisited / rank @@
+Normal rank
@@ Property / cites work @@
+An algebraic generalization of Frege structures -- binding algebras
+Normal rank
@@ Property / cites work @@
+Q4716271
@@ Property / cites work: Q4716271 / rank @@
+Normal rank
@@ Property / cites work @@
+Nominal techniques in Isabelle/HOL
@@ Property / cites work: Nominal techniques in Isabelle/HOL / rank @@
+Normal rank
@@ Property / cites work @@
+General Bindings and Alpha-Equivalence in Nominal Isabelle
+Normal rank