On the Role of Names in Reasoning about λ-tree Syntax Specifications

DOI10.1016/j.entcs.2008.12.122zbMath1337.68076OpenAlexW2054675474MaRDI QIDQ2804945

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

zbMATH Keywords

bisimulationlogical frameworkpi-calculusnominal techniquesgeneric judgments

Mathematics Subject Classification ID

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

Uses Software

• Abella

Cites Work

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

This page was built for publication: On the Role of Names in Reasoning about λ-tree Syntax Specifications