有效候选人何积丰教授



所有跟贴·加跟贴·新语丝读书论坛http://www.xys.org/cgi-bin/mainpage.pl

送交者: email 于 2005-6-02, 17:57:59:

回答: 中国科学院院士增选有效候选人的公告 由 email 于 2005-6-02, 17:09:35:

http://www.iist.unu.edu/~jifeng/

He Jifeng


Address
International Institute of Software Technology
United Nations University
P.O.Box 3058, Macau


Telephone
712930

Present Position
Professor of Computer Science (1986-), East China Normal Univ.
Professor of Computer Science (1996-), Shanghai Jiao Tong Univ.
Senior Research Fellow (1998-), International Institute of Software Technology, United Nations Univ.


Previous Position
Senior Research Fellow (1984-1998), Oxford University Computing Laboratory, Programming Research Group


Expertise
My research interest lies in the sound methods of specification of computer systems, communications, application and standards, and the techniques for designing and implementing those specifications in software and/or hardware, with high reliability and at low cost.

Publications


"A Heuristic Approach for Optimum Testing Sequences" (in Chinese) Proceedings of the Conference on Computer- Aided Design (1978).

"A Fixed Point Principle for Proving the Correctness of Programs" (in Chinese) Proceedings of 1979 China Computer Congress (1979).

"Operations on Recursive Languages" (in Chinese) Journal of East China Normal University (1980).

"Predicate transformer of a programming language with goto statement" Acta Informatica (1983)

"Design of a Computer-Based Business Management System" (in Chinese) Journal of Computer and its Application (1983).

"Program Transformers" (1) (in Chinese) Journal of East China Normal University (1983).

"Program Transformers" (2) (in Chinese) Journal of East China Normal University (1983).

"Software Design of an Information Processing System" (in Chinese) Computing Engineering (1983)

"System Design and Development of MIS" (in Chinese) Software Engineering and Application (1984).

"Development Strategy for MIS' (in Chinese) Journal of Minicomputer System (1984).

"Principles of Operating Systems' (text-book) (in Chinese) Engineering Industry Publishing House (1985).

"Design of an Office Automation System" (in Chinese) Proceedings of Design of Applicative Software (1985).

"Weakest Prespecifications" part-1.(with C.A.R.Hoare) Fundamenta Informaticae IX (1986) 51-84.

"Weakest Prespecifications" part-2.(with C.A.R.Hoare) Fundamenta Informaticae IX (1986) 217-252

"Algebraic specification and proof of properties of a mail service" (with C.A.R.Hoare) Program Specification and Transformation, edited by L.Meertens (1986) 411-429.

"Data Refinement Refined" (with C.A.R. Hoare and J.W.Sanders) Lecture Notes in Computer Science 213 (1986), 187-196.

"Prespecification in Data Refinement" (C.A.R. Hoare and J.W.Sanders) Information Processing Letters 25 (2) (1987), 71-76.

"Algebraic specification and proof of a distributed recovery algorithm" (with C.A.R.Hoare) Distributed Computing Vol 2 (1987), 1-12

"Design and proof of a mail service" (with C.A.R. Hoare) Proceedings of the 6th International Phoenix Conference on Computers and Communications (1987), 272-276.

"Laws of Programming" (with others) Comm. of the ACM 30(8): 672-686 (1987).

"Weakest Prespecification" (with C.A.R.Hoare) Info. Processing Letters 24 (1987).

"Specification of The X.25 protocol: a case study in CSP" Proceedings of the distributed computing workshop, edited by C.A.R. Hoare (1990).

"Process Refinement" in the Theory and Practice of Refinement, edited by M.J.McDermid, Butterworth, (1989), 37--59.

"Specification and Design of Interactive Systems with various Interfaces" Oxford University Monograph (1989).

"Simulation and Process Refinement" Formal Aspects of Computing (1989) 1:229-241.

"Categorical Semantics of Programming Language" (with C.A.R. Hoare) Invited Address. LNCS 442 edited by M. Mislove and M. Main, (1990).

"Specification, Analysis and Refinement of Interactive Processes' (with Bernard Sufrin), in "Formal Methods in Human-Computer Interaction", edited by M. Harrison and H. Thimbleby, Cambridge University Press (1990) 153-201.

"Various simulations and refinements" Proceedings of REX Workshop on Distributed System Design, Springer-Verlag, Lecture Notes in Computer Science 430 (1990) 340-361.

"A theory of Synchrony and Asynchrony" (with Mark Josephs and C.A.R. Hoare) Programming Concepts and Methods, edited by M. Broy and C.B. Jones. 459-479, (1990).

"An Approach to Verifiable Compiling Specification and Prototyping" (with J. Bowen and P. Pandya) In Lecture Notes of Computer Science 456, 45-60, (1990)

"An algebraic Approach to Verifiable Compiling Specification and Prototyping of the PROCOS Level 0 Programming Language" (with C.A.R. Hoare, J. Bowen and P. Pandya) Esprit '90 Conference Proceedings, Kluwer Academic Publishers, 804-819, 1990.

"Refinement Algebra Proves Correctness of Compiler" (with Tony Hoare) Keynote address in BCS Refinement Workshop, Springer-Verlag, (also in Lecture Notes of International Summer School at Marktorbdorf), 1990.

"Pre-Adjunctions in Order Enriched Categories" (with C.A.R. Hoare and C.E. Martin) in Mathematical Structure in Computer Science 1, 141-158, (1991).

"A Theory of State-based Parallel Programming by Refinement" (with Xu Qiwen) in Proceedings of BCS FACS 4th Refinement Workshop, 326-359, (1991)

"A case study in formally developing state-based parallel programming - the Dutch National Torus" (with Xu Qiwen) in Proceedings of BCS FACS 5th Refinement Workshop, 301-319, (1992)

"Semantics and Implementation of a real time programming language" (with J. Bowen) in Proceedings of 1992 Euromicro conference, 110-116, (1992).

"From Algebra to Operational Semantics" (with Tony Hoare) in Information Processing Letters 45, 75-80, (1993).

"Real-time refinement: Semantics and application" (with D. Scholefield and H. Zedan) in Lecture Notes of Computer Science 711 693-703. (1993)

"A Provable Hardware Implementation of occam" (with I. Page and J. Bowen) in Lecture Notes of Computer Science 683, 214-226, (1993).

"Hybrid Parallel Programming and Implementation of Synchronised Communication" in Lecture Notes of Computer Science 711, 537-547, (1993).

"Normal Form Approach to Compiler Design" (with Tony Hoare and A Sampaio) Acta Informatica (30), 701-739, (1993)

"From CSP to Hybrid System" in "Hoare Festschrift" (edited by B. Roscoe). 171-191, (1993).

"Programs to Hardware" (with J. Bowen) in Proceedings of FME'1993.

"Laws of parallel programming with shared variables" (with Xu Qiwen) in Proceedings of BCS FACS 6th Refinement Workshop, (1994).

"A real-time Programming Language" (with R. Hale) in "Towards a provably correct system" (1994).

"A Predicative Semantics for the Refinement of Real-Time Systems" in Lecture Notes of Computer Science 802, 230-249, (1994).

"Hardware Compilation" (with I. Page and J. Bowen) in "Towards a provably correct system" (1994).

"Simulation Approach to Hardware Compilation" (with J. Zheng). in Lecture Notes of Computer Science 863, 336-351, (1994).

"Provably Correct Systems." (with Tony Hare and others). in Lecture Notes of Computer Science 863, 288-335, (1994).

" A specification-oriented semantics for the refinement of real-time systems" (with D. Scolefield and H. Zedan) Theoretical Computer Science 131 (1), 219-241, (1994).

"Design and Optimisation of a correct compiler" (with J. Bowen) Formal Aspect of Computing 6, 643-658, (1994)

"Towards Verified Systems" (with J. Bowen) In C.Mitchell and V. Stavridou (eds.) The Mathematics of Dependable Systems, Oxford University Press, The Institute of Mathematics and Its Application Conference Series, volume 55, 23-48, (1995).

"Deriving Handshake Modules for a multi-target hardware compiler" (with W. Luk and J. Brown) The proceedings of the DCC workshop, Sweden, (1996).

"Algebraic Programming of BSP" Proceedings of Euro Parallel, 1996.

"Specification and design of a coherent cached memory" Proceedings of FACS'96, (1996).

"Algebraic laws of shared-state concurrency" (with Xu Qiwen, and W.P. de Roever) Formal Aspect of Computing, 149-174, (1997)

"Probabilistic models for guarded command language" Science of computer programming, 28: 171-192, (1997).

"Linking theories in probabilistic programming" (with Tony Hoare) in Proceedings of SBLP'97, (1997).

"Unifying theories of concurrency" (with Tony Hoare) Key address in EuroPar'97, 1997

"Algebraic derivation of an operational semantics" (with Tony Hoare and A. Sampiao) in "Milner's Festschrift", (edited by Plotkin). MIT press, 1997

"The rely-Guarantee Method for Verifying Shared Variable Concurrent Programs" (with Q. Xu and W. de Roever), Formal Aspect of Computing, 149-174, (1997)

"A theory of probabilistic programming" (with Tony Hoare) the journal of Information Sciences, (1998).

"Formal Reasoning with Verilog HDL" (with G. Pace), in the Proceeding of Formal Method in Hardware Design, Spain, (1998).

"Trace model of pointers" (with Tony Hoare), in M. Broy (ed):Logic of Programming, (1998)

"Unifying theories of healthiness conditions" (with Tony Hoare), in the Proceeding of Relational Programming'98, (1998).
Book:

"Provably Correct System: design and implementation of communication language", McGraw Hill Publisher, (1994).

"Unifying theories of programming" (with Tony Hoare), Prentice-Hall International, (1998)



所有跟贴:


加跟贴

笔名: 密码(可选项): 注册笔名请按这里

标题:

内容(可选项):

URL(可选项):
URL标题(可选项):
图像(可选项):


所有跟贴·加跟贴·新语丝读书论坛http://www.xys.org/cgi-bin/mainpage.pl