Strong normalisation in the \(\pi\)-calculus

DOI10.1016/j.ic.2003.08.004zbMath1101.68705OpenAlexW2028016184MaRDI QIDQ598201

Kohei Honda, Martin Berger, Nobuko Yoshida

Publication date: 6 August 2004

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

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

zbMATH Keywords

Concurrency theoryThe \(\pi\)-calculusStrong normalisationType theory

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items

Characteristic bisimulation for higher-order session processes, Eager functions as processes, A Logical Interpretation of the λ-Calculus into the π-Calculus, Preserving Spine Reduction and Types, Mobile Processes and Termination, Conflation Confers Concurrency, Unnamed Item, The true concurrency of differential interaction nets, On the potential advantages of exploiting behavioural information for contract-based service discovery and composition, Termination in a π-calculus with subtyping, Linear logical relations and observational equivalences for session-based concurrency, Formalising Java RMI with explicit code mobility, Behavioural equivalences for dynamic web data, Responsiveness in process calculi, Typed event structures and the linear \(\pi \)-calculus, An exact correspondence between a typed pi-calculus and polarised proof-nets, Interpreting a finitary pi-calculus in differential interaction nets, Typing termination in a higher-order concurrent imperative language, Termination in higher-order concurrent calculi, A type system for lock-free processes, On the relative expressiveness of higher-order session processes, Ensuring termination by typability, Linearity and bisimulation, On the Relative Expressiveness of Higher-Order Session Processes, Unnamed Item, Corecursion and Non-divergence in Session-Typed Processes, Full Abstraction in a Subtyped pi-Calculus with Linear Types, Static Livelock Analysis in CSP, Partial Orders, Event Structures and Linear Strategies, A Process-Model for Linear Programs, Genericity and the \(\pi\)-calculus, Type-Based Security for Mobile Computing Integrity, Secrecy and Liveness, Probabilistic π-Calculus and Event Structures

Uses Software

• Automath
• PIPER
• PLAN

Cites Work

• Linear logic
• \(\pi\)-calculus, internal mobility, and agent-passing calculi
• Computational interpretations of linear logic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Some congruence properties for \(\pi\)-calculus bisimilarities
• A calculus of communicating systems
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• A calculus of mobile processes. II
• On the expressiveness of internal mobility in name-passing calculi
• Proofs as processes
• On the \(\pi\)-calculus and linear logic
• On reduction-based process semantics
• On full abstraction for PCF: I, II and III
• Full abstraction for PCF
• Game-theoretic analysis of call-by-value computation
• The name discipline of uniform receptiveness
• Functions as processes
• Games and full completeness for multiplicative linear logic
• A generic type system for the Pi-calculus
• Types as models
• A uniform type structure for secure information flow
• PLAN
• Intensional interpretations of functionals of finite type I
• 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
• Unnamed Item
• Unnamed Item