A proof theory for generic judgments
From MaRDI portal
Publication:5277739
DOI10.1145/1094622.1094628zbMath1367.03059OpenAlexW2032234226MaRDI QIDQ5277739
Publication date: 12 July 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1094622.1094628
proof searchhigher-order abstract syntaxgeneric judgmentsreasoning about operational semantics\(\lambda\)-tree syntax\(\nabla\)-quantifier
Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Cut-elimination and normal-form theorems (03F05)
Related Items
The undecidability of proof search when equality is a logical connective, Fresh logic: Proof-theory and semantics for FM and nominal techniques, Proof checking and logic programming, A Logical Encoding of Timed $$\pi $$-Calculus, Nominal SOS, Unnamed Item, SOS formats and meta-theory: 20 years after, When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus, Nominal abstraction, A formalized general theory of syntax with bindings, A Survey of the Proof-Theoretic Foundations of Logic Programming, Constraint handling rules with binders, patterns and generic quantification, A logical framework with higher-order rational (circular) terms, Cut elimination for a logic with induction and co-induction, Unnamed Item, The Abella Interactive Theorem Prover (System Description), A formalized general theory of syntax with bindings: extended version, a-Logic With Arrows, Structural recursion with locally scoped names, Proof Pearl: Abella Formalization of λ-Calculus Cube Property, Relating State-Based and Process-Based Concurrency through Linear Logic, PNL to HOL: from the logic of nominal sets to the logic of higher-order functions, Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism, \(\mathrm{HO}\pi\) in Coq, Relating state-based and process-based concurrency through linear logic (full-version), A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs, On the Expressivity of Minimal Generic Quantification, Reasoning in Abella about Structural Operational Semantics Specifications, On the Role of Names in Reasoning about λ-tree Syntax Specifications, A new connective in natural deduction, and its application to quantum computing, A congruence rule format for name-passing process calculi, A new connective in natural deduction, and its application to quantum computing, Formalizing Operational Semantic Specifications in Logic, A semantics for nabla, Constructing weak simulations from linear implications for processes with private names, A case study in programming coinductive proofs: Howe’s method, Mechanized metatheory revisited, A proof theory for model checking, Undecidability of Model Checking in Brane Logic, A Proof Theoretic Approach to Operational Semantics, Specifying Properties of Concurrent Computations in CLF, A Meta Linear Logical Framework, Contextual equivalence for inductive definitions with binders in higher order typed functional programming
