Relating state-based and process-based concurrency through linear logic (full-version)

DOI10.1016/j.ic.2008.11.006zbMath1181.68168OpenAlexW1999161312MaRDI QIDQ731895

Iliano Cervesato, Andrej Scedrov

Publication date: 9 October 2009

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2008.11.006

zbMATH Keywords

process algebralinear logicconcurrencysecurity protocolsmultiset rewriting

Mathematics Subject Classification ID

Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Grammars and rewriting systems (68Q42) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Related Items

On concurrent behaviors and focusing in linear logic, A proof theoretic view of spatial and temporal dependencies in biochemical systems, Back to futures, Fairness and communication-based semantics for session-typed languages, Logical approximation for program analysis, Unnamed Item, Unnamed Item, Unnamed Item, Bounded memory Dolev-Yao adversaries in collaborative systems, A framework for linear authorization logics, Unnamed Item, Nested session types, Collaborative planning with confidentiality, Relating reasoning methodologies in linear logic and process algebra, A message-passing interpretation of adjoint logic, Session-typed concurrent contracts

Uses Software

• Maude
• Pict
• Freshml
• NRL
• Lolli

Cites Work

• Linear logic
• Forum: A multiple-conclusion specification logic
• Conditional rewriting logic as a unified model of concurrency
• The chemical abstract machine
• A calculus for cryptographic protocols: The spi calculus
• Linear logic as a logic of computations
• Logic programming in a fragment of intuitionistic linear logic
• The complexity of Horn fragments of linear logic
• Proofs as processes
• On the \(\pi\)-calculus and linear logic
• On proof normalization in linear logic
• First-order linear logic without modalities is NEXPTIME-hard
• Encoding transition systems in sequent calculus
• A new natural structural congruence in the pi-calculus with replication
• A categorical linear framework for Petri nets
• Uniform proofs as a foundation for logic programming
• The NRL Protocol Analyzer: An Overview
• Communicating sequential processes
• Using encryption for authentication in large networks of computers
• Transition and cancellation in concurrency and branching time
• From Petri nets to linear logic
• Encryption as an abstract data-type
• Petri Nets as Token Objects
• FreshML
• A proof theory for generic judgments
• Lectures on Concurrency and Petri Nets
• Types for Proofs and Programs
• Perspectives of System Informatics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item