dual-session Exploration of session type duality coinductive definition (functional and relational) inductive definition of Lindley and Morris (equivalence to coinductive definition) naive tail recursive definition (equivalence to coinductive definition)