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

DOI10.1016/J.ENTCS.2008.12.122MaRDI QIDQ2804945zbMATH OpenOpenAlexFDO

Authors 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

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)

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

Cites work

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

Cited in

(2)

• External and internal syntax of the \(\lambda \)-calculus
• A logic for reasoning about generic judgments

Describes a project that uses

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)