Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types

DOI10.46298/LMCS-18(3:27)2022MaRDI QIDQ5043586zbMATH OpenOpenAlexFDO

Authors Luca Ciccone, Luca Padovani

Publication date 6 October 2022

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2108.01503

zbMATH Keywords

coinductioninductioninference systemslivenesssafetysession types

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Fair subtyping for open session types
• Type-Based Analysis for Session Inference (Extended Abstract)
• Fair subtyping for multi-party session types
• Context-free session type inference
• Session types as generic process types

Cites work

• Defining liveness
• Depending on session-typed processes
• Fair subtyping for multi-party session types
• Fair subtyping for open session types
• Fair testing
• Fairness and hyperfairness
• Fundamental properties of infinite trees
• Generalizing inference systems by coaxioms
• Handbook of modal logic
• scientific article; zbMATH DE number 1701362 (Why is no real title available?)
• scientific article; zbMATH DE number 7037626 (Why is no real title available?)
• scientific article; zbMATH DE number 3972158 (Why is no real title available?)
• scientific article; zbMATH DE number 48630 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 7699430 (Why is no real title available?)
• scientific article; zbMATH DE number 7699432 (Why is no real title available?)
• Introduction to bisimulation and coinduction
• Proving Liveness Properties of Concurrent Programs
• Recognizing safety and liveness
• Results on the propositional \(\mu\)-calculus
• Semantic subtyping, dealing set-theoretically with function, union, intersection, and negation types
• Subtyping for session types in the pi calculus
• Subtyping Supports Safe Session Substitution
• Testing equivalences for processes
• Using higher-order contracts to model session types

Cited in

(1)

• A sound and complete characterization of fair asynchronous session subtyping

Describes a project that uses

Uses Software

• GitHub

This page was built for publication: Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types

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