In this talk, I’ll my work on a formalisation of the session-typed functional language GV using Agda. There are two main challenges which set formalising session-typed languages apart from, e.g., formalising the standard lambda calculus: First, session-typed are linear. Enforcing linearity in a formalisation is a difficult task. Worse, most available frameworks for binding (ACMM, autosubst, Ott, to name a few) do not support linear types, leaving us to solve a more difficult problem with fewer tools. My approach formalising GV is based on a combination of ACMM with Quantitative Type Theory. Second, the proof of progress for session-typed languages is complex, as configurations of processes are identified up to a structural congruence (for instance, (P | Q) = (Q | P)). While the reduction relation itself is easy to formalise, proving progress requires us to prove that we always have a pair of processes ready to communicate somewhere within the configuration. I am tackling this problem by taking some inspiration from abstract machines, and developing a syntax for configurations which is is always in normal form and which enforces the invariants which I need to prove progress.