# Latest News

#### 09 November 2021

##
Fair Termination of Binary Sessions

The paper **Fair Termination of Binary Sessions** (Ciccone & Padovani, 2022), written with Luca Ciccone, has been accepted
at the *49*^{th} annual Symposium on Principles of
Programming Languages (POPL 2022). In this work we study a type
system that ensures the **termination** of binary sessions under
strong fairness assumptions. The type system is the first using
**fair subtyping** (Padovani, 2013; Padovani, 2016; Ciccone & Padovani, 2021), a liveness-preserving refinement of the classical subtyping
relation for session types that has been studied extensively in the
last years but was never applied in a type system. FairCheck is a
proof-of-concept implementation of the type system described in the
paper. You can read a draft of the paper
online
before it is officially published.

#### 07 October 2021

##
FairCheck

The GitHub repository of
FairCheck is now publicly
available. FairCheck is a proof-of-concept implementation of a type
checker for a calculus of binary sessions such that well-typed
processes are guaranteed to be fairly terminating. Fair termination
is a generalized form of termination whereby all infinite executions
of a process are deemed unrealistic because they violate some
fairness assumption. The type system on which FairCheck is based is
also the first one using **fair subtyping** (Padovani, 2013; Padovani, 2016; Ciccone & Padovani, 2021), a liveness-preserving refinement of
the subtyping relation for session types.

#### 29 April 2021

##
Inference Systems with Corules for Fair Subtyping

The paper **Inference Systems with Corules for Fair Subtyping and
Liveness Properties of Binary Session Types** (Ciccone & Padovani, 2021), written with Luca Ciccone, has been accepted
at the *48*^{th} International Colloquium on Automata,
Languages, and Programming (ICALP 2021). In this work we use
generalized inference
systems to
specify combined safety and liveness properties of *dependent
session types* mixing induction and coinduction. All the results
have been formalized in Agda and are available on
GitHub. Too bad
the conference will be online only.

All posts…