Formal verification of concurrent programs in type theory. - Shen-Wei Yu (1999)