For three distinct and complete achievements: 1) LCF, the mechanization of DanaScott's Logic of Computable Functions, probably the first theoretically based yet practical tool for machine assisted proof construction (see AutomatedTheoremProving); 2) ML [MlLanguage], the first language to include PolymorphicTypeInference together with a type-safe exception-handling mechanism; 3) CCS [CalculusOfCommunicatingSystems], a general theory of concurrency. In addition, he formulated and strongly advanced full abstraction, the study of the relationship between operational and DenotationalSemantics.