Behavioral equivalence in the polymorphic pi-calculus

DOI10.1145/337244.337261MaRDI QIDQ5487879zbMATH OpenOpenAlexFDO

Authors Benjamin C. Pierce, Davide Sangiorgi

Publication date 12 September 2006

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://repository.upenn.edu/cis_reports/95

zbMATH Keywords

parametric polymorphism in message-based concurrent programmingpolymorphic lambda-calculus

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Genericity and the \(\pi\)-calculus
• Behavioral polymorphism and parametricity in session-based communication
• Typed behavioural equivalences for processes in the presence of subtyping
• scientific article; zbMATH DE number 1956508
• Typed behavioural equivalences for processes in the presence of subtyping

Cited in

(28)

• The security pi-calculus and non-interference
• Assigning types to processes
• A generic type system for the pi-calculus
• The name discipline of uniform receptiveness
• Bisimulation and coinduction enhancements: a historical perspective
• Types and full abstraction for polyadic -calculus
• Behavioural equivalences for dynamic web data
• Full abstraction for polymorphic \(\pi \)-calculus
• A type system for lock-free processes
• Genericity and the \(\pi\)-calculus
• Subtyping for session types in the pi calculus
• safeDpi: a language for controlling mobile code
• On hierarchical communication topologies in the -calculus
• Typed behavioural equivalences for processes in the presence of subtyping
• A well-behaved LTS for the pi-calculus (abstract)
• Propositions as sessions
• Extending modal transition systems with structured labels
• Bounded polymorphism in session types
• A Complete Characterization of Observational Equivalence in Polymorphic λ-Calculus with General References
• The name discipline of uniform receptiveness (extended abstract)
• On confluence in the -calculus
• Typed behavioural equivalences for processes in the presence of subtyping
• Linear logical relations and observational equivalences for session-based concurrency
• Encoding distributed areas and local communication into the -calculus
• Behavioral polymorphism and parametricity in session-based communication
• Types for ambient and process mobility
• Security types for dynamic web data
• An exact correspondence between a typed pi-calculus and polarised proof-nets

Describes a project that uses

Uses Software

• MWB
• Pict

This page was built for publication: Behavioral equivalence in the polymorphic pi-calculus

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