Constructing weak simulations from linear implications for processes with private names
From MaRDI portal
Publication:5236556
DOI10.1017/S0960129518000452zbMath1447.68008OpenAlexW2932898195MaRDI QIDQ5236556
Publication date: 9 October 2019
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0960129518000452
Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Proof-theoretic aspects of linear logic and other substructural logics (03F52)
Related Items
An Analytic Propositional Proof System on Graphs, A System of Interaction and Structure III: The Complexity of BV and Pomset Logic, Unnamed Item, Unnamed Item
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Linear logic
- Nominal abstraction
- \(\pi\)-calculus, internal mobility, and agent-passing calculi
- Models for concurrency: Towards a classification
- The equational theory of pomsets
- A calculus of mobile processes. II
- Proofs as processes
- On the \(\pi\)-calculus and linear logic
- Encoding transition systems in sequent calculus
- Nominal logic, a first order theory of names and binding
- A theory of bisimulation for the \(\pi\)-calculus
- Uniform proofs as a foundation for logic programming
- Mutually Testing Processes
- Proof search specifications of bisimulation and modal logics for the π-calculus
- A system of interaction and structure IV
- A Local System for Classical Logic
- A system of interaction and structure V: the exponentials and splitting
- Behavioural Analysis of Sessions Using the Calculus of Structures
- Formalising the pi-calculus using nominal logic
- Characterising Testing Preorders for Finite Probabilistic Processes
- Logic Programming with Focusing Proofs in Linear Logic
- Semantics for Specialising Attack Trees based on Linear Logic
- The Consistency and Complexity of Multiplicative Additive System Virtual
- De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
- Divergence and unique solution of equations
- A proof theory for generic judgments
- A system of interaction and structure
- A System of Interaction and Structure II: The Need for Deep Inference
- Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types
- A deep inference system with a self-dual binder which is complete for linear lambda calculus
- Linear logic propositions as session types
- Refinement of actions and equivalence notions for concurrent systems
