AWARDEE OF TECHNOLOGICAL SCIENCES PRIZE

LI WEI

Abstract

Li Wei, male, computer scientist, was bron in Beijing on June 8, 1943.
In 1966, he graduated from Beijing University with a major in Mathematics. He received his Ph. D in Computer Science from University of Edinburgh, UK in 1983. He is professor at Beijing University of Aeronautics and Astronautics since 1986. He was elected to be an academician in the Chinese Academy of Science in 1997.
In the early 1980, Li Wei worked on formal semantics of concurrent programs using the structural operational semantic approach. He has published more than 20 papers on this subject including works on: building the structural operational semantics for parallel computations, and communication, synchronization, and exception handling between tasks or processes of practical concurrent programming languages, such as, Ada and Occam. He also defined an operational semantics for the packages, critical sections, and the parallel execution of Petri nets in the languages of Ada, Addison and COSY. He pioneered the establishment of a translation theory between concurrent programming languages, and created an approach to construct translations between those languages. He also designed the formal translations between several well-known concurrent computational models such as Ada, CSP and CCS, and proved their correctness.
Having studied the role of versions of software products in software development processes and the non-monotonicity of common sense in epistemic processes, Li Wei formally introduced the sequences of formal theories and the limits of those sequences into the first order logic in the early 1990s. He formalized the concept of strategies for generating sequences of formal theories. He constructed a Gentzen style proof system to devive the revisions of a formal theory by counter-example or refutation. He built strategies for generating “conjecture and refutation” processes and “inductive inference and refutation” processes; and proved their convergence. He has published more than 30 papers on these subject, and pioneered the introduction of analysis of sequences and limits into mathematical logic.
As chief engineer, he led his research team in the design of a multi-stack architecture for supporting both Lisp and Prolog execution from 1989 to 1991. This team bulit China first logical inference computer along with an integrated knowledge program development environment in 1992. His research team also designed a networks based on extended computer buses in 1995, built a scalable network computer cluster in 1996, and invented three patents in these subjects from 1993 to 1996.
Li Wei has published more than 60 scientific papers in English and 40 papers in Chinese. He received the second National Science Prize awarded by the State Council in 1995, and several First and Second Technologcial Progress Prizes awarded by the Ministry of Aviation and Aerospace.