Pages that link to "Item:Q5277739"

The following pages link to A proof theory for generic judgments (Q5277739):

Displaying 43 items.

• Nominal abstraction (Q617715) (← links)
• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions (Q714797) (← links)
• Relating state-based and process-based concurrency through linear logic (full-version) (Q731895) (← links)
• SOS formats and meta-theory: 20 years after (Q877025) (← links)
• A congruence rule format for name-passing process calculi (Q1012125) (← links)
• A formalized general theory of syntax with bindings (Q1687739) (← links)
• Cut elimination for a logic with induction and co-induction (Q1948276) (← links)
• A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
• \(\mathrm{HO}\pi\) in Coq (Q2031410) (← links)
• The undecidability of proof search when equality is a logical connective (Q2134939) (← links)
• Mechanized metatheory revisited (Q2323447) (← links)
• A proof theory for model checking (Q2331070) (← links)
• Fresh logic: Proof-theory and semantics for FM and nominal techniques (Q2372191) (← links)
• Proof checking and logic programming (Q2628296) (← links)
• A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs (Q2802499) (← links)
• On the expressivity of minimal generic quantification (Q2804937) (← links)
• Reasoning in Abella about structural operational semantics specifications (Q2804943) (← links)
• On the role of names in reasoning about \(\lambda\)-tree syntax specifications (Q2804945) (← links)
• Undecidability of model checking in brane logic (Q2864500) (← links)
• Specifying properties of concurrent computations in CLF (Q2871839) (← links)
• A meta linear logical framework (Q2871843) (← links)
• Contextual equivalence for inductive definitions with binders in higher order typed functional programming (Q2875221) (← links)
• Structural recursion with locally scoped names (Q3016213) (← links)
• Nominal SOS (Q3178277) (← links)
• A Logical Encoding of Timed $$\pi $$-Calculus (Q3453652) (← links)
• The Abella Interactive Theorem Prover (System Description) (Q3541698) (← links)
• (Q4415240) (← links)
• Constraint handling rules with binders, patterns and generic quantification (Q4592722) (← links)
• Proof Pearl: Abella Formalization of λ-Calculus Cube Property (Q4916060) (← links)
• Relating State-Based and Process-Based Concurrency through Linear Logic (Q4917995) (← links)
• (Q4972733) (← links)
• Formalizing Operational Semantic Specifications in Logic (Q4982629) (← links)
• (Q5014803) (← links)
• A semantics for nabla (Q5236555) (← links)
• Constructing weak simulations from linear implications for processes with private names (Q5236556) (← links)
• A case study in programming coinductive proofs: Howe’s method (Q5236557) (← links)
• A Proof Theoretic Approach to Operational Semantics (Q5262970) (← links)
• a-Logic With Arrows (Q5403474) (← links)
• Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism (Q5437034) (← links)
• A new connective in natural deduction, and its application to quantum computing (Q5918648) (← links)
• A new connective in natural deduction, and its application to quantum computing (Q5925711) (← links)
• When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus (Q6041667) (← links)
• A Survey of the Proof-Theoretic Foundations of Logic Programming (Q6063891) (← links)