On the role of names in reasoning about -tree syntax specifications

DOI10.1016/J.ENTCS.2008.12.122zbMATH Open1337.68076OpenAlexW2054675474MaRDI QIDQ2804945FDOQ2804945

Alwen Tiu

Publication date: 6 May 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2008.12.122

Recommendations

• Nominal logic, a first order theory of names and binding
• scientific article; zbMATH DE number 2242589
• Nominal abstraction
• Foundations of nominal techniques: logic and semantics of variables in abstract syntax
• External and internal syntax of the \(\lambda \)-calculus

zbMATH Keywords

pi-calculusbisimulationnominal techniquesgeneric judgmentslogical framework

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• The Abella Interactive Theorem Prover (System Description)
• Nominal logic, a first order theory of names and binding
• A calculus of mobile processes. II
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• The \(\pi\)-calculus: A theory of mobile processes
• Unification under a mixed prefix
• Cut-elimination for a logic with definitions and induction
• Practical Programming with Higher-Order Encodings and Dependent Types
• A theory of bisimulation for the \(\pi\)-calculus
• Reasoning in Abella about structural operational semantics specifications
• A proof search specification of the \(\pi\)-calculus
• Proof search specifications of bisimulation and modal logics for the π-calculus
• A proof theory for generic judgments
• Term Rewriting and Applications
• A Proof-Theoretic Approach to Logic Programming
• Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations
• Barendregt’s Variable Convention in Rule Inductions
• A logic for reasoning about generic judgments

Uses Software

• Abella

This page was built for publication: On the role of names in reasoning about \(\lambda\)-tree syntax specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2804945)