ACM通信
约翰·雷诺兹(1935 - 2013
专注于程序和编程语言逻辑基础研究的计算机科学家约翰·c·雷诺兹于4月28日去世。
来源:卡内基梅隆大学
卡内基梅隆大学(CMU)计算机科学教授约翰·c·雷诺兹(John C. Reynolds)于4月28日因心脏病发作去世。
雷诺兹于1961年获得哈佛大学理论物理学博士学位。据CMU计算机科学学院院长兼计算机科学大学教授兰迪·布莱恩特(Randy Bryant)说，在阿贡国家实验室(Argonne National Laboratory)工作期间，雷诺兹开始意识到自己的热情在于计算。布莱恩特说，因此，雷诺兹“成为了一名非常成功的计算机科学家，专注于程序和编程语言的逻辑基础。”1970年至1986年，他在雪城大学担任信息科学教授，之后加入CMU，成为计算机科学系(CSD)的教员。他于2012年退休，但继续担任惩教署名誉教授。
他还曾在奥尔胡斯大学(丹麦)、爱丁堡大学、伦敦帝国理工学院、微软研究院(剑桥)和玛丽女王伦敦大学(英国)担任访问职位。
根据他的CSD主页雷诺兹的研究集中在“编程语言和指定程序行为的语言的设计，定义这些语言的语义的数学工具，以及证明程序满足其规范的方法。”另一个感兴趣的领域是“类型的语义”。在过去的15年里，我们看到了各种类型系统的发现，它们极大地扩展了我们对类型是什么以及如何使用类型的概念。我的目标是理解这些系统的意义，并找到它们都属于哪种类型的一般概念。”
此外，Reynolds对“类al戈尔语言的设计、定义和证明方法感兴趣，它将命令式构造与强大的过程机制结合起来，同时保留块结构和局部变量的概念”。
同样是CSD计算机科学教授的罗伯特·哈珀(Robert Harper)将雷诺兹描述为“我们许多人的导师和激励者，为科学家、学者和绅士提供了一个很好的例子。”约翰对细节的细致关注和对卓越不妥协的坚持是我们所有人都想模仿的科学家的最佳品质的例证。”在2010年一封提名雷诺兹为日本奖的信中，哈珀写道:“雷诺兹在学术计算机科学领域的工作的深远影响现在正在计算机行业中感受到。Java和c#编程语言中的泛型类型的概念起源于Reynolds 1978年关于多态λ微积分的论文。命令式程序的验证工具现在在软件行业中广泛使用，这很大程度上得益于Reynolds在程序规范和验证方面的工作，特别是分离逻辑这一极具独创性的概念，该概念通过控制组件之间的干扰，允许对大型软件系统进行模块化验证。”
CMU的科比说:“约翰在他的职业生涯中做出了许多重要的贡献。有趣的是，他在2002年与彼得·奥赫恩(Peter O'Hearn)等人合作的分离逻辑研究尤其突出。分离逻辑提供了一种正式的方法来推理我们可能认为的“正常程序”，即通过改变存储在内存中的值来操作的程序，但内存被划分为独立的块，因此我们可以独立地推理不同的程序组件。我只希望我在67岁时所做的工作是我最好的工作之一。”
雷诺兹曾是《美国ACM通讯》和《美国ACM杂志》等期刊的编委会成员。2001年，他被任命为ACM院士。他于2003年获得ACM SIGPLAN编程语言成就奖，并于2010年获得英国计算机学会颁发的Lovelace奖章。
科比补充道:“我们也会记住约翰这种愉快的精神，他高标准的道德标准和深刻的智慧。我们将非常怀念他。”
没有发现记录