for Computer Science
Institute of Software
Chinese Academy of Sciences
Fax: +86 10 62661627
am a research professor in the Laboratory for
Computer Science, Institute of Software,
Chinese Academy of
Sciences. The laboratory is committed to basic as well as
application-oriented research in computer science, with focus on fundamental
software research. It is still expanding and have several positions, including
visiting positions, available. If you are interested in doing research in
Beijing, or just coming for a visit, then please contact me or other people in
the lab whose areas are close to yours.
Research interests: Concurrency, Process algebras, Value-passing, Mobility, Model
checking, Modal logics and mu-Calculus, Tools and algorithms for concurrent
systems, Formal methods.
- H. Lin, A Predicate mu-Calculus for Mobile Ambients. Journal of Computer Science and
Technology. Vol.20, No. 1, pp.95-104, 2005. [paper.ps.gz
] Talks given
at China-Germany Joint Workshop on Theoretical Computer Science, Shanghai, Oct.
15-17, 2003, and International Workshop on Formal Methods and Security,
Nanjing, May 17-20, 2004. [slides.ps]
] An extended
abstract of this paper appeared in TAPSOFT'95, Aarhus, Denmark, May
1995. LNCS 915. pp. 187-201.
Lin and Wang Yi, Axiomatising Timed Automata. Acta Informatica.
38, 277-305 (2002). Springer-Verlag. [paper.ps.gz] An extended abstract of
this paper appeared in FST&TCS'2000, New Delhi, December 2000.
LNCS 1974, pp.277-289.
Hennessy, H. Lin and J. Rathke, Unique Fixpoint Induction for
Message-Passing Process Calculi. Science of Computer Programming
41(3), 241-275 (2001). Elsevier.
Lin, Model Checking Value-passing Processes. 8th Asia-Pacific
Software Engineering Conference (APSEC'2001), Macau, December 4-7,
Ingolfsdottir and H. Lin, A Symbolic
Approach to Value-passing Processes. Chapter 7 of Handbook of
Processes Algebra. Elsevier. 2001. [paper.ps.gz]
Lin and Wang Yi, A Proof System for
Timed Automata. FOSSACS'2000, Berlin, March/April 2000. LNCS
1784, pp.208-222. [paper.ps.gz]
Lin, Computing Bisimulations for Finite-Control pi-Calculus. Journal
of Computer Science and Technology, Vol.15, No. 1, 2000. [paper.ps.gz]
Lin, Inference Systems for Observation Equivalences in the pi-Calculus
(in Chinese). Science in China (Series E), Vol.29, No.5,
Lin, "On-the-fly" Instantiation of Value-passing Processes.
FORTE/PSTV'98, Paris, November 1998. pp. 215-230. Kluwer Academic
Lin, Complete Proof Systems for Observation Congruence in
Finite-Control pi-Calculus. ICALP'98, Aalborg, Denmark, August
1998, pp. 443-454. LNCS 1443. Springer. [paper.ps.gz]
Hennessy and H. Lin, Unique Fixpoint Induction for Message- passing
Process Calculi. CATS'97, Sydney, Australia, Feb. 1997, pp.
Lin, On Removing Unguarded Recursions in The pi-Calculus (in Chinese).
Journal of Software. Vol. 8, pp. 321-326. 1997.
Hennessy and H. Lin, Proof Systems for Message-passing Process Algebras.
Formal Aspects of Computing, Vol. 8, pp. 379-407. 1996. Springer. [paper.ps.gz]
Lin, Symbolic Transition Graph with Assignment. CONCUR'96,
Pisa, Italy, August 1996. pp. 50-65. LNCS 1119. [paper.ps.gz]
Lin, PAM: A Process Algebra Manipulator. Formal Method in
Systems Design, Vol. 7, No. 3, pp. 243-259, 1995. Kluwer Academic
Publishers. [paper.ps.gz] An extended abstract of
this paper appeared in CAV'91, Aalborg, Denmark, July 1991. LNCS
575. pp. 136-146.
Hennessy and H. Lin, Symbolic Bisimulations. Theoretical
Computer Science, Vol. 138, pp. 353 - 389, 1995. Elsevier.
Lin, Unique Fixpoint Induction for Mobile Processes. CONCUR'95,
Philadelphia, USA, August 1995, pp. 88-102. LNCS 962. [paper.ps.gz]
Lin, On Implementing Unique Fixpoint Induction for Value-passing Processes.
TACAS'95, Aarhus, Denmark, May 1995. [paper.ps.gz]
Lin, Proof Systems for the pi-Calculus (in Chinese). Advances in
Theoretical Computer Science, Nov 1994. pp. 1-5.
Lin, Symbolic Bisimulations and Proof Systems for the Pi-Calculus. Sussex University Computer Science
Report 1994:07. [paper.pdf]
Lin, Procedural Implementation of Algebraic Specifications. ACM
Transactions on Programming Languages and Systems, Vol. 15 No. 5, pp.
876-895, 1993. ACM Press.
Lin, A Verification Tool for
Value-Passing Processes. 13th IFIP Symposium on Protocol
Specification, Testing and Verification, Liege, Belgium, May 1993. pp.
79-92. North-Holland. [paper.ps.gz]
Lin, An Interactive Proof Tool for
Process Algebras. 9th Symposium on Theoretical Aspects of Computer
Science, Paris, Feb. 1992. LNCS 577.
Lin and M.C. Pong, Modeling Multiple Inheritance
with Colimits. Formal Aspects of Computing, Vol. 2 No.4, pp.
301-311, 1990. Springer.