Strong normalisation in the -calculus

DOI10.1016/J.IC.2003.08.004zbMATH Open1101.68705OpenAlexW2028016184MaRDI QIDQ598201FDOQ598201

Authors: Nobuko Yoshida, Martin Berger, Kohei Honda 

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

Recommendations

• Strong normalization in the \(\pi \)-calculus with intersection and union types
• scientific article; zbMATH DE number 2163051
• scientific article; zbMATH DE number 1088033
• Proving strong normalisation via non-deterministic translations into Klop's extended lambda-calculus
• Strong normalization from weak normalization in typed \(\lambda\)-calculi

zbMATH Keywords

The \(\pi\)-calculusConcurrency theoryStrong normalisationType theory

Mathematics Subject Classification ID

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

Cites Work

• PLAN: a packet language for active networks
• On full abstraction for PCF: I, II and III
• Full abstraction for PCF
• Title not available (Why is that?)
• Functions as processes
• Title not available (Why is that?)
• Title not available (Why is that?)
• Linear logic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A calculus of mobile processes. II
• Computational interpretations of linear logic
• A calculus of communicating systems
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Title not available (Why is that?)
• Title not available (Why is that?)
• On reduction-based process semantics
• \(\pi\)-calculus, internal mobility, and agent-passing calculi
• Game-theoretic analysis of call-by-value computation
• Games and full completeness for multiplicative linear logic
• Intensional interpretations of functionals of finite type I
• Title not available (Why is that?)
• Some congruence properties for \(\pi\)-calculus bisimilarities
• The name discipline of uniform receptiveness
• Title not available (Why is that?)
• Title not available (Why is that?)
• Types as models: model checking message-passing programs
• Title not available (Why is that?)
• A generic type system for the \(\pi\)-calculus
• Title not available (Why is that?)
• A uniform type structure for secure information flow
• On the expressiveness of internal mobility in name-passing calculi
• Title not available (Why is that?)
• Title not available (Why is that?)
• Proofs as processes
• On the \(\pi\)-calculus and linear logic
• Strong normalisation of cut-elimination in classical logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (39)

• Formalising Java RMI with explicit code mobility
• An exact correspondence between a typed pi-calculus and polarised proof-nets
• Genericity and the \(\pi\)-calculus
• Divergence and unique solution of equations
• Termination in higher-order concurrent calculi
• Mobile Processes and Termination
• Static Livelock Analysis in CSP
• Typed event structures and the linear \(\pi \)-calculus
• Eager functions as processes
• Interpreting a finitary pi-calculus in differential interaction nets
• Termination in a \(\pi\)-calculus with subtyping
• Probabilistic \(\pi\)-calculus and event structures
• Characteristic bisimulation for higher-order session processes
• Behavioural equivalences for dynamic web data
• Conflation confers concurrency
• Safe session-based concurrency with shared linear state
• Strong normalization in the \(\pi \)-calculus with intersection and union types
• Uniform strong normalization for multi-discipline calculi
• A Logical Interpretation of the λ-Calculus into the π-Calculus, Preserving Spine Reduction and Types
• Full abstraction in a subtyped pi-calculus with linear types
• Title not available (Why is that?)
• On the potential advantages of exploiting behavioural information for contract-based service discovery and composition
• Corecursion and non-divergence in session-typed processes
• A Process-Model for Linear Programs
• Ensuring termination by typability
• Type-based security for mobile computing integrity, secrecy and liveness
• Linear logical relations and observational equivalences for session-based concurrency
• Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions
• On the relative expressiveness of higher-order session processes
• On the relative expressiveness of higher-order session processes
• Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination
• Strong normalization of barrecursive terms without using infinite terms
• Responsiveness in process calculi
• Typing termination in a higher-order concurrent imperative language
• Linearity and bisimulation
• Divergence and unique solution of equations
• Partial Orders, Event Structures and Linear Strategies
• The true concurrency of differential interaction nets
• A type system for lock-free processes

Uses Software

• Automath
• PIPER
• PLAN

This page was built for publication: Strong normalisation in the \(\pi\)-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q598201)