# Intrinsically-Typed Mechanized Semantics for Session Types

## TL;DR

This paper introduces an executable, intrinsically typed small-step semantics for a functional session type calculus, implemented in Agda, ensuring type soundness and progress through mechanization.

## Contribution

It presents the first mechanized, intrinsically typed semantics for a realistic session type calculus including recursion, subtyping, and asynchronous communication.

## Key findings

- Proves type preservation and progress in Agda implementation
- Models asynchronous communication with encoding
- Ensures soundness through mechanized semantics

## Abstract

Session types have emerged as a powerful paradigm for structuring communication-based programs. They guarantee type soundness and session fidelity for concurrent programs with sophisticated communication protocols. As type soundness proofs for languages with session types are tedious and technically involved, it is rare to see mechanized soundness proofs for these systems. We present an executable intrinsically typed small-step semantics for a realistic functional session type calculus. The calculus includes linearity, recursion, and recursive sessions with subtyping. Asynchronous communication is modeled with an encoding. The semantics is implemented in Agda as an intrinsically typed, interruptible CEK machine. This implementation proves type preservation and a particular notion of progress by construction.