迈克尔·约翰·考德威尔·戈登（Michael John Caldwell Gordon，FRS，1994），1948年2月28日-2017年8月22日
Michael John Caldwell Gordon (FRS 1994), 28 February 1948 -- 22 August 2017
摘要：
Michael Gordon是交互式定理证明和硬件验证领域的先驱。在20世纪70年代，他的愿景是正式验证系统设计，使用数学和逻辑证明其正确性。他在现实世界的计算机设计中展示了他的想法。他的学生将工作扩展到不同的领域，如浮点算法的验证，概率算法的验证和源代码的验证翻译，以纠正机器码。他当选为英国皇家学会于1994年，他继续生产杰出的研究，直到退休。他的成就包括他在爱丁堡大学的工作，帮助创建爱丁堡LCF，第一个交互式定理证明器，以及ML家族的函数式程序设计语言。他采用高阶逻辑作为验证的一般形式，表明它可以指定从门级到处理器级的硬件设计。它被证明是计算机科学和数学中许多问题的理想形式。他的工具和技术在形式化验证领域产生了巨大的影响。
英文摘要：
Michael Gordon was a pioneer in the field of interactive theorem proving and hardware verification. In the 1970s, he had the vision of formally verifying system designs, proving their correctness using mathematics and logic. He demonstrated his ideas on real-world computer designs. His students extended the work to such diverse areas as the verification of floating-point algorithms, the verification of probabilistic algorithms and the verified translation of source code to correct machine code. He was elected to the Royal Society in 1994, and he continued to produce outstanding research until retirement. His achievements include his work at Edinburgh University helping to create Edinburgh LCF, the first interactive theorem prover of its kind, and the ML family of functional programming languages. He adopted higher-order logic as a general formalism for verification, showing that it could specify hardware designs from the gate level right up to the processor level. It turned out to be an ideal formalism for many problems in computer science and mathematics. His tools and techniques have exerted a huge influence across the field of formal verification.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
