何積豐

何積豐(3張)

1943年8月5日，何積豐出生於上海市。

1965年2月，何積豐從復旦大學數學系畢業，並被分配到華東師範大學工作，是上海高校中第一批從事計算機科學研究的人員。

1980年7月，何積豐作為訪問學者，被華東師範大學被派往美國舊金山大學進修，專攻計算機應用，課餘時間裏，他常常到遠離舊金山的斯坦福大學和另一所名牌大學去旁聽課程，斯坦福大學的導師被他打動，不久，何積豐被批准進入斯坦福大學學習（至1981年7月）。

1984年12月，何積豐在英國牛津大學計算機實驗室任客座教授、高級研究員（至1998年7月）。

何積豐 演講 報告(8張)

1986年8月，何積豐晉升為華東師範大學教授 ^[5]  。

1995年8月，何積豐被聘為華東師範大學博士生導師。

1998年7月，何積豐任聯合國大學國際軟件技術研究所高級研究員。

2001年11月，何積豐擔任華東師範大學軟件學院院長。

2002年12月，何積豐成為華東師範大學首批終身教授。

2005年，何積豐當選中國科學院院士。

2016年，何積豐受聘為華東師範大學計算機科學與軟件工程學院院長。

2019年，何積豐受聘為同濟大學特聘教授，入職同濟大學交通運輸工程學院 ^[19-20]  。

①創建程序統一理論，奠定了軟件語義元理論基礎，開創了軟件理論的新學派。

何積豐與圖靈獎獲得者Hoare教授創造性地提出了軟件的程序統一理論，解決了程序語義的一致性問題，奠定了軟件語義元理論基礎，開創了程序統一理論學派，出版了英文專著《Unifying Theories of Programming》，該文獻他引超過800次。程序統一理論已被國際上公認為研究各類程序語言的一種標準方法。自2006年起，每兩年舉辦一次程序統一理論國際學術研討會，包括牛津大學、約克大學、巴黎11大等在內的世界著名研究機構從事序統一理論的相關研究。

②創新軟件開發方法學，建立了數據精化完備理論，被國際上譽為“面向模型軟件開發的一個里程碑”。

針對軟件開發各階段模型正確性問題，何積豐創建了數據精化完備理論，首次提出了數據精化的“程序分解算子”與“上下仿真映照對”方法，將規範語言與程序語言看成是同一類數學對象，採用“關係代數”作為程序和軟件規範的統一數學模型，在此框架中建立了求解規範方程的演算法則。該成果被國際計算機科學界譽為“面向模型軟件開發的一個里程碑”。

③開拓可信嵌入式軟件設計理論與技術，促進了方法與技術在安全攸關行業領域的應用。

何積豐創造性地開拓和發展了基於模型的可信軟件開發與驗證研究領域，建立了正確性系統的可證理論與方法，解決了可信嵌入式系統構造與驗證技術的若干關鍵問題，並應用於軌道交通、汽車電子、航天控制等安全攸關行業，推動了相關產業發展。 ^[18] 

二零一七年香山科學會議，何積豐在世界上首次提出“可信人工智能”，自此世界各地開始廣泛關注人工智能的安全可信問題。 ^[29] 

截至2018年，何積豐出版英文專著2部，在國際期刊和會議上發表論文160餘篇，他引4000餘次 ^[6]  。

He Jifeng and C.A.R. Hoare. "Algebraic specification and proof of a distributed recovery algorithm" Distributed Computing Vol 2, 1-12, (1987) ^[33] 

He Jifeng and C.A.R. Hoare. "Categorical Semantics of Programming Language". Invited talk in Workshop of the mathematical foundation of semantics of programming languages, U.S.A. 1988. Lecture Notes in Computer Sciences 442. Springer, (1990) ^[34] 

He Jifeng. "Hybrid Parallel Programming and Implementation of Synchronised Communication" Lecture Notes of Computer Science 711, 537-547, Springer, (1993) ^[35] 

He Jifeng. "A Predicative Semantics for the Refinement of Real-time Systems" Lecture Notes of Computer Science 802, 230-249, Springer, (1994) ^[39] 

He Jifeng and C.A.R. Hoare. “Linking theories in probabilistic programming” Information Sciences, vol 119, 205-218, (1999) ^[36] 

He Jifeng "An Algebraic Approach to Verilog Programming" Lecture Notes in Computer Science 2757, 65-81, (2002) ^[40] 

He Jifeng and Xu Qiwen. "Advanced features of Duration Calculus and their applications in sequential hybrid programs" Formal Aspect of Computing Vol 15, 84-99, (2003) ^[37] 

He Jifeng "Linking theories of concurrency" (Invited talk) In Proceedings of CSP'25, Springer, (2004) ^[42] 

Jifeng He, Jeff W. Sanders: Unifying Probability. UTP 2006: 173-199 ^[41] 

Jifeng He, Qin Li: A new roadmap for linking theories of programming and its applications on GCL and CS Science of Computer Programming 162 (2018) 3–34 ^[38] 

截至2020年，何積豐先後擔任國家自然科學基金委重大研究計劃、科技部973計劃、863計劃主題項目首席科學家，領銜國家自然科學基金委創新研究羣體 ^[6]  。

截至2020年，何積豐先後以唯一完成人獲得國家自然科學獎二等獎和上海市科技進步獎一等獎各1項，以項目第一完成人榮獲上海市科技進步獎特等獎 ^[26]  ，以第一完成人獲省部級科技進步獎與科技成果獎一等獎4項 ^[6]  。

何積豐努力踐行服務社會的創新人才培養理念，始終堅持以科學的態度從事教學、科學研究服務並反哺教學，強調對青年道德品性的培養。他探索軟件人才培養和科學研究的新路子，倡導“以學生為中心，以市場為導向，以創新求發展”的國際化辦學理念，並構建了新穎的創新型軟件人才分層培養一體化機制 ^{[6]  [9]}  。

何積豐為本科生開設了第一門由院士主講的通識教育課程《計算機文化》，並梳理了自己多年的科研成果，為研究生開設了《程序統一理論》課程 ^[10]  。

2006年何積豐獲得上海市教學名師稱號，2013年9月獲得第三屆上海市教育功臣稱號 ^[11]  ，他還被評為上海市教書育人楷模。

何積豐是信息領域領軍專家，被國際計算機科學界譽為面向模型軟件開發方法的奠基石。他在安全軟件設計方面的論著被國際軟件界廣泛引用。他率先提出關係程序設計語言，這項工作被歐洲計算機界認為是繼過程語言、函數程序、邏輯程序之後的第四類程序語言的先驅，他因而被歐洲軟件界權威人士贊之為“軟件設計技術上的一座里程碑”。（中華人民共和國工業和信息化部評）

“何老師始終把學術事業和祖國的命運與黨領導的事業密切地聯繫在一起，為自己能夠在國家發展、學術發展和整個社會的進步中發揮作用而感到自豪。” ^[16]  （華東師範大學黨委書記童世駿評）

“何積豐教授在極具應用前景的重要領域中的計算科學方面做出了大量的基礎性貢獻”。 ^[18]  （圖靈獎獲得者Hoare 評）

“我發明的關係演算工作主要歸功於何積豐的研究”。 ^[18]  （圖靈獎獲得者Dijkstra 評）

“在過去十五年，何積豐是牛津大學程序研究領域取得成功的驅動力”。 ^[18]  （英國科學技術委員會給政府的報告 評）

“何積豐在軟件工程的科學理論與工業實踐方面做出了奠基性的工作⋯他發明並開發了計算機系統、通信與標準的精確規範（數學）理論與技術，能以低成本的方式構建高可靠的軟件與硬件系統”。 ^[18]  （英國皇家工程院院士McDermid 評）

何積豐認為，可信人工智能，主要包含三個要素——人、信息、物理。而所謂的安全，也包括數據安全、技術安全和系統安全。判斷是否可信的先決條件之一，是設立關於可信的度量標準。比如，要求數據本身真實可信。數據可信之外是技術可信和系統可信。當人工智能程序或產品發生錯誤時，對錯誤或會發生的結果具備可解釋性。在其特性或參數發生攝動時，相關係統和技術依舊具備品質指標保持不變的性能，即魯棒性等。

在他看來，智慧城市和智慧製造已經成為了推動可信AI落地最主要的兩大應用場景。智慧城市也就是社會治理的智能化，大數據分析已經在發揮很大的作用。智慧製造方面也在逐步推進。

“從長遠來看，我們希望人工智能不是一個簡單的工具箱，而是與人類在同一個閉環內相互互動，幫助我們做決策。”何積豐認為，人工智能的發展軌跡可能不是一個線性的變化，而是會迎來指數性的增長機會，“未來或許會有一個爆發性的拐點出現。” ^[24]