NDLI: On the Preciseness of Subtyping in Session Types

Please wait, while we are loading the content...

Declarative Software Development: Distilled Tutorial

Parametricity and Proving Free Theorems for Functional-Logic Languages

Bijective Collection Encodings and Boolean Operations with Hereditarily Binary Natural Numbers

Design and Implementation of a Multithreaded Virtual Machine for Executing Linear Logic Programs

Proofs in continuation-passing style: normalization of Gödel's System T extended with sums and delimited control operators: Distilled Tutorial

A Type Theoretic Specification of Partial Evaluation

Continuations, Processes, and Sharing

Elimination of Square Roots and Divisions by Partial Inlining

Real-Time Matching of Antescofo Temporal Patterns

On the Declarative Structure of Quantum Concepts: States and Observables (Distilled Tutorial)

Proving Operational Termination of Declarative Programs in General Logics

Theories of Homomorphic Encryption, Unification, and the Finite Variant Property

On the Preciseness of Subtyping in Session Types

BiFluX: A Bidirectional Functional Update Language for XML

Declarative Game Programming: Distilled Tutorial

Bidirectional Elaboration of Dependently Typed Programs

Exact Intersection Type Abstractions for Safety Checking of Recursion Schemes

Structure-Preserving Compilation: Efficient Integration of Functional DSLs into Legacy Systems

Organising Low-Level Programs using Higher Types

Unveiling and Veiling Information in Programs

On Combining Backward and Forward Chaining in Constraint Logic Programming

Assertion-based Debugging of Higher-Order (C)LP Programs

Decision Procedures for Proving Inductive Theorems without Induction

Experimental Evaluation of a State-Of-The-Art Grounder

Heuristics Entwined with Handlers Combined: From Functional Specification to Logic Programming Implementation

Database Queries that Explain their Work

On the Preciseness of Subtyping in Session Types

Content Provider	ACM Digital Library
Author	Chen, Tzu-Chun Yoshida, Nobuko Dezani-Ciancaglini, Mariangiola
Abstract	Subtyping in concurrency has been extensively studied since early 1990s as one of the most interesting issues in type theory. The correctness of subtyping relations has been usually provided as the soundness for type safety. The converse direction, the completeness, has been largely ignored in spite of its usefulness to define the greatest subtyping relation ensuring type safety. This paper formalises preciseness (i.e. both soundness and completeness) of subtyping for mobile processes and studies it for the synchronous and the asynchronous session calculi. We first prove that the well-known session subtyping, the branching-selection subtyping, is sound and complete for the synchronous calculus. Next we show that in the asynchronous calculus, this subtyping is incomplete for type-safety: that is, there exist session types T and S such that T can safely be considered as a subtype of S, but T ≤ S is not derivable by the subtyping. We then propose an asynchronous subtyping system which is sound and complete for the asynchronous calculus. The method gives a general guidance to design rigorous channel-based subtypings respecting desired safety properties.
Starting Page	135
Ending Page	146
Page Count	12
File Format	PDF
ISBN	9781450329477
DOI	10.1145/2643135.2643138
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2014-09-08
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Π-calculus Completeness and soundness Session types Subtyping
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

On the preciseness of subtyping in session types (2014)

Preciseness of Subtyping on Intersection and Union Types?

On the Preciseness of Subtyping in Session Types

Towards concurrent type theory

Declarative interpretations of session-based concurrency

Using session types for reasoning about boundedness in the $$\pi $$ π -calculus

A Mechanical Soundness Proof for Subtyping Over Recursive Types

A process calculus for Web data with subtyping

Deadlock and lock freedom in the linear π-calculus

On the Preciseness of Subtyping in Session Types

Similar Documents

On the preciseness of subtyping in session types (2014)

Preciseness of Subtyping on Intersection and Union Types?

On the Preciseness of Subtyping in Session Types

Towards concurrent type theory

Declarative interpretations of session-based concurrency

Using session types for reasoning about boundedness in the $$\pi $$ π -calculus

A Mechanical Soundness Proof for Subtyping Over Recursive Types

A process calculus for Web data with subtyping

Deadlock and lock freedom in the linear π-calculus

On the Preciseness of Subtyping in Session Types