References. Syntax and Models of a non-Associative Composition of Programs and Proofs (Munch-Maccagnoni, 2013) Classical notions of computation and the Hasegawa-Thielecke theorem (Mangel, Melliès, Munch-Maccagnoni, 2025)