A short paper entitled “Toward a Mechanically Proven Model of Google Drive” was presented at CAL 2015 in Hammamet, Tunisia, 14--15 May 2015.