Title: Mechanised formal reasoning about modular programs