Michel__Bidoit
Behavioural satisfaction and equivalence in concrete model categories
Observer complete definitions are behaviourally coherent
Proving behavioural theorems with standard first-order logic
Proving the Correctness of Behavioural Implementations