林晖闵简介和详细信息
林晖闵的主要贡献林晖闵研究员长期从事计算机程序特别是并发程序的形式语义和形式方法的研究。在进程代数的验证工具、信息传递过程的语义理论、π-演算的公理化等方面取得突破。他的主要贡献包括:
1.设计并实现了世界上第一个通用的进程代数验证工具。
进程代数的实际应用离不开计算机辅助工具的支持。80年代后期，出现了一批进程代数的验证工具(如CWB、PSF、LOTOSphere等。).它们的共同局限是每种工具只适合于特定的过程演算。这种局限性阻碍了验证工具的推广和应用。如何克服这一限制，是当时国际进程代数界面临的一大挑战。这些验证工具之所以不能通用，根本原因是缺乏一种能够描述不同进程演算的语义，并且能够被计算机理解的通用语言。经过反复比较不同的演算，并考虑到在计算机上实现的可能性，林提炼出一种元语言，可以描述各种进程演算的公理语义，可读性好。在此基础上，实现了一个通用的交互式进程代数验证工具PAM[1]。只要将这种元语言描述的过程演算的定义输入到PAM中，就可以得到这种演算的证明者。PAM可以同时接受多个不同的演算，并为每个演算生成多个证明窗口。这是世界上第一个通用的进程代数证明工具。1993年，林利用当时刚刚得到的信息传递过程证明系统的理论成果，对PAM进行了扩展，开发出了迄今为止世界上唯一可以处理信息传递过程的验证工具[2]。
林晖闵2。与轩尼诗教授合作，提出并独立发展了“符号相互模拟”理论，在信息传递过程的研究上取得了突破。并发理论研究的核心问题是进程间的通信(消息传输)。然而，在传统进程代数的理论研究中，为了便于数学处理，通信被简化为简单的同步。从消息传输过程到简单同步演算的过渡是通过一个变换来完成的，核心步骤是将输入动作翻译成遍历数据域的选择操作数。当数据域为无穷大时，是一个无穷大的操作数，但在实际问题中，数据域往往是无穷大的。这种无限操作数的引入，使得进程代数的许多理论成果无法应用，难以使用耗费大量人力物力开发的验证工具解决实际问题。
林晖闵·林晖闵与英国苏塞克斯大学的轩尼诗教授合作提出了“符号相互模拟理论”[3]，其基本出发点是直接建立消息传递过程的语义理论，而不依赖于上述变换。该理论将输入视为抽象动作而非实例化，从而避免了数据字段的无限性带来的无限性。这里要克服的主要困难是，抽象输入动作执行后，过程项可能包含自由变量，即成为开放项，而传统过程代数理论使用的语义模型只能解释没有自由变量的封闭项。在[3]中引入了“符号转移图”作为语义模型，并在此基础上建立了符号互模拟理论。在[4]中，进一步建立了一个相对完整的消息传输过程相互模拟的证明体系。
3.彻底解决了π-演算的有限公理化问题。
为了描述移动通信，ACM图灵奖获得者Milner教授及其合作者在1989正式提出了π-演算(也称为“移动进程演算”)。π演算研究中的一个基本问题是刻画进程间的相互模拟等价关系。在π-演算的原始文献中，只给出了恒(地)强互模拟的公理系统。4年后，π-演算的提出者之一发表了一般强互模拟的完整公理体系，但未能解决弱互模拟更难的公理问题。这个问题已经成为π演算研究中激烈竞争的一个热点。
林晖闵-林建立了π-演算的符号互模拟理论，并于1995年5月在第六届国际软件开发理论与实践会议上发表了π-演算晚期和早期弱互模拟的完整证明体系[7]。同年8月在美国费城举行的第六届并发理论国际会议上引用这一成果，国际同行指出:“到目前为止，π-演算的晚期弱互模拟的公理化只是在[Lin95]中借助符号互模拟的概念得到的。”(见附件“引文摘录”)
为了推理π-演算中递归定义的无限进程，林在第六届国际并发理论大会上把“进程抽象”的结构引入π-演算，提出了π-演算独特的不动点归纳法[8]，并在1998年7月第35届ICALP大会上进一步发表了π-演算与有限控制弱互模拟的完整证明体系[9]。这一成果彻底解决了π-演算的有限公理化问题，使我国在这一极具竞争力的研究方向上处于国际领先地位。
此外，近年来还有十余所欧美高等院校和科研机构，包括INRIA、巴黎师范大学、爱丁堡大学、宾夕法尼亚大学等。
长期从事并发理论和形式化方法的研究。他设计并实现的交互式证明系统PAM是世界上第一个通用的进程代数验证工具。与国际同行合作，提出并自主开发了“符号互模拟”理论。解决了π演算和时间自动机的有限公理化问题。这些成果被国内外同行在公开发表的文献中广泛引用，促进了这些领域的发展。其工作获得中国科学院自然科学奖一等奖1996，国家自然科学奖二等奖1999。在进程代数的验证工具、信息传递过程的语义理论、π-演算的公理化等方面取得突破性进展。主要贡献有:1996，林获中国科学院自然科学一等奖(唯一获奖者)。他学风严谨，勇于开拓创新，取得了一系列国际领先的成果，得到了国际同行的认可，是国际上有影响力的计算机科学家。
研究方向长期从事计算机程序特别是并发程序的形式语义和形式化方法的研究。
林晖闵的学习经历是1982。2月获得福州大学计算机系计算机软件专业学士学位。
1986年6月在中国科学院软件研究所获得计算机科学理论博士学位。
工作经历65438+9月0986-1987 65438+2月英国爱丁堡大学计算机科学基础实验室。
1988 65438+10月-1990 3月中国科学院软件研究所副教授。
65438+4月0990-65438+4月0993英国苏塞克斯大学研究员
1993中国科学院软件研究所研究员。
1994 112室，中国科学院软件研究所博士生导师。
1999中国科学院软件研究所计算机科学国家重点实验室主任
社会*** 1990软件学报编辑委员会
1994中国计算机联合会理论计算机科学专业委员会副主席
1997中国科技大学研究生院教授
1999中国计算机学报中英文版编辑委员会。
获奖情况他在进程代数的验证工具、信息传递过程的语义理论、π-演算的公理化等方面取得突破性进展，主要贡献有:1996林获中国科学院自然科学一等奖(唯一获奖者)。他学风严谨，勇于开拓创新，取得了一系列国际领先的成果，得到了国际同行的认可，是国际上有影响力的计算机科学家。
论学术贡献的代表性
1.林，潘:一个过程代数操纵器。FormalMethodsinSystemDesign，第7卷，第3期，第243-259.1995页。kluweracademicpublishers . 2 . h . Lin，AVerificationToolforValue-passing process代数。IFIPTransactionsC-16:协议规范、测试和验证，第79-92.1993页。北荷兰。
林晖闵3.m .轩尼诗和h。林象征性的装糊涂。理论计算机科学，第138卷，第353-389页.
4.M和H.Lin，证明系统形式传递过程代数。《计算形式谱》第8卷，第397-407.1996页。施普林格出版社。
5.H.Lin，带分配的符号转换图，proc . 7 thint . conf . oncurrencytheory，意大利比萨，8月26-29日，1996。计算机科学第1119卷，第50-56页。施普林格出版社。
6.价值传递过程的动态实例化。proc . jointinternational conferenceesonformaldescriptiontechniquesfordistributedsystemsandcommunication p协议和协议规范、测试和验证，法国巴黎，11月1998 . PP . 215-230 . kluweracademicpublishers。
7.林，高等演算中的完全推理系统。proc . 6 hinternationalljointconferenceontheorandpracticeofsaferadevelopment，丹麦奥胡斯，邮编:1995。计算机科学讲座，第915卷，第187-201页。施普林格出版社。
8.林，UniqueFixpointInductionforMobileProcesses。proc . 6 hinternationalconconferenceoncurrencytheory .美国费城，8月1995。计算机科学讲义，第962卷，第88-102页。施普林格出版社。
9.林，completeproofsystemsforobservation同余infinitecontrolpi-微积分。第25届丹麦Aalb语言与程序设计国际研讨会论文集，7月1998。计算机科学第1443卷，第443-454页。施普林格出版社。
10.林，代数规范的程序实现。acmtransactionsonprogrammingslanguagesandsystems，第15卷，第5期，第876-895页。
攻击欺诈
林晖闵毫不客气地抨击了那些在科技界制造虚假名声的人。“我现在真的不敢相信科学进步奖了。”在2010政协科协界别联组讨论会上，林晖闵委员震惊了。这位62岁的中国科学院院士，计算机软件和理论方面的权威专家说，他曾被邀请审查一个项目，结果发现获奖材料的内容是虚假的。林晖闵呼吁，要加大力度，彻底改革科技奖励的评选机制，结束目前造假授奖的乱象，以维护科技奖励的公信力，实现科技评价制度的公平公正。否则，将严重挫伤科研人员的积极性，损害国家的创新精神。
林晖闵说，“现在拿一个奖去卖，连企业家都怀疑，人们会问:你花了多少钱去评估这个奖？”
林晖闵的话引起了广泛的共鸣。有委员表示，公众很清楚科技奖存在的问题，这是一件非常不好的事情。委员们的这种经历在科技界普遍存在。九三学社主要针对大学教师和科研院所的科技人员做了一个调查。在7699份有效样本中，70.3%的受访者认为目前我国科技成果的鉴定和奖励结果“取决于成果的水平以及一定的公关活动”，而只有12.5%的人认为“主要取决于成果的真实水平”。
业内专家表示，历年来，国家最高科技奖和三个奖项的一等奖基本没有争议，但以下奖项有争议。“这说明数量多了，质量没那么高。就算没有造假，我们国家的科技水平真的有那么高吗？”虽然获奖材料中的这一写法达到了世界先进水平，并且解决了世界级难题，但这些奖项中有哪些可以进行国际比较呢？其实是有水分的。“现在的问题是，行业协会、学会、社会组织颁发的奖项也很难让公众信服。问题的根源在于学术界的过度行政化。管理人员不了解学术界的情况，只能用量化的标准来衡量，研究人员不得不遵从，因为管理人员有权分配资源。
人物语录数学。这个名字不好听。小学读的书叫算术，不叫数学，很有中国特色，和计算机密切相关。算术是教你如何做计算的方法，例如计算多位数乘法。那怎么做呢？你有一套方法。你要把表格背出来，然后你就知道了。比如你把142乘以98，你就知道怎么去歪斜位置了。老师会教你这条规则。单位乘以单位，然后乘数的单位乘以被乘数的十位数。那你得记得带着。这些都是机械的规则。所谓的机械法则，就是计算机能理解。电脑是机械的东西。不像人，有脑子，那么聪明。电脑很蠢。所以你可以乘，可以除，可以编程。我认为在中学甚至小学从事计算机教育是非常重要的，因为将来整个社会都会普及计算机，将来没有人会离不开计算机。因为不是所有的学生将来都能上大学的计算机系，即使上了大学，也只有少部分会上计算机系，所以中小学生计算机教育的普及极其重要，这对整个社会和未来的发展都非常重要。这是学生毕业走向社会，适应新信息社会挑战的关键一步。回想起来，至少我越年轻，算法思维越好，思维方式越适应编程，所以就想到了算术。我记得小时候是怎么想的，怎么一步一步想出来的。然后到了中学以后，可能会有一些不同。我中学学的是代数，几何，代数在中国是传统。几何学基本上来自欧洲。涉及到分析推理的训练，我的理解和几何。就是你有算法的想法，你怎么做，一步一步来，把一个复杂的问题分解成机械的步骤。另外就是你要有一个严谨的思维。在你把它分解之后，你最终应该能够把它做好。我觉得学生在编程的时候，尽量笨一点，就像电脑一样，可以编出来。
有各种各样的原因。一个是工作上的。第一次出国的时候，我觉得可能英国人和西方人都很伟大，一些现代计算机理论都是他们发展出来的。所以我觉得他们应该是伟大的，好像他们比我们优秀，而不是像我们中国人脑子里可能有的那么大，是不是比我们有钱。但和他们接触后，我觉得不是那样的。作为一个人，没有太大的区别。1987年底，我的亲生父亲去世了，所以对我触动很大。我想我应该回来尽我所能。
主持人:林老师，您是软件专家。你会玩游戏吗？为什么？林老师:不是，游戏软件有一个特点。首先，它是一个非常好的电脑设备。计算机运行得非常快。它可以使图像非常美丽和迷人。然后电脑的反应速度比人快很多，可以编程让你永远打不过电脑。然后是编写游戏软件的人，他的主要任务就是让游戏引人入胜，一步步让你越来越想玩。这是做游戏软件的人的工作，因为他靠这个谋生，靠这个卖钱。问题是你能有多少时间玩？几年前，有一两个来自英国、美国和德国的孩子，他们24小时玩耍，整夜不睡，不愿睡觉。那是他们着迷的点，结果出来后，整个人都散架了。年轻人没有自制力，很容易呆在里面吃东西。
主持人:他大学选的是计算机专业，应该能更好的玩这个游戏，或者说他是打算设计的。他可能知道更多里面的东西，所以他怎么会放弃呢？
林老师:学了软件之后，就不怎么喜欢玩电脑游戏了。为什么？游戏软件是从事编程和软件的人编写的。自己做软件就知道，这些游戏都是我们同行设计编译的。你在那里玩游戏很热情，感觉自己很有能力。你能敲下来吃的，其实是那些设计软件的人设计的陷阱。你觉得自己被戏弄了，就是被同龄人戏弄了。
主持人:刚才我们听林老师讲了这么多关于网络游戏的内容。学生们有什么问题想和林老师交流吗？
学生:你好，林老师！我想问你一个问题，就是我以后会致力于研究游戏软件吗？如果我现在不花时间在这个游戏上，去了解它的优缺点，当我以后想编译游戏软件的时候，我对这个玩家的喜恶一无所知，也就是说，我会很难做到。你能帮我回答这个问题吗？如何权衡利弊？
林老师:我认为这是你真正需要做的两件事。设计游戏软件和玩游戏不一样。就像每天看电视，不代表你以后要造电视。我觉得以后你一定要先学会怎么做软件，怎么做图像，图像处理，图形处理，然后你一定要学会编程，编程的基本功。要学习这些东西，你需要学习它们。你在大学高三的时候学过，然后你需要你中学的这些图形和图像。很多都是数学的东西。你需要把他们一层一层的弄下来，然后等你毕业了，比如你会去一家搞游戏软件的公司。那时候你就真的会出软件了，和玩这个游戏很不一样。
数学研究所召开中科院林晖闵院士专题报告会。
中国科学院林晖闵院士在数学学院学术报告厅举行专题报告会。数学学院副院长、院长范耿华，党委书记陈世权，副书记褚勇、牛牧，副院长徐荣聪、叶东毅，师生代表等近200人参加了报告会。报告会由副校长兼数学学院院长范耿华主持。林晖闵院士是我院77级数学专业的校友。1999当选中国科学院院士。林晖闵院士精辟合理的报告令与会师生着迷，赢得阵阵掌声。报告取得了圆满成功。