Huimin
LIN
Laboratory
for Computer Science
Institute of Software
Chinese Academy of Sciences
P.O.Box 8718
Beijing 100190
P.R.China
Fax: +86 10 62661627


I
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
applicationoriented 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, Valuepassing, Mobility, Model
checking, Modal logics and muCalculus, Tools and algorithms for concurrent
systems, Formal methods.
Publications
 H. Lin, A Predicate muCalculus for Mobile Ambients. Journal of Computer Science and
Technology. Vol.20, No. 1, pp.95104, 2005. [paper.ps.gz
] Talks given
at ChinaGermany Joint Workshop on Theoretical Computer Science, Shanghai, Oct.
1517, 2003, and International Workshop on Formal Methods and Security,
Nanjing, May 1720, 2004. [slides.ps]
] An extended
abstract of this paper appeared in TAPSOFT'95, Aarhus, Denmark, May
1995. LNCS 915. pp. 187201.
 H.
Lin and Wang Yi, Axiomatising Timed Automata. Acta Informatica.
38, 277305 (2002). SpringerVerlag. [paper.ps.gz] An extended abstract of
this paper appeared in FST&TCS'2000, New Delhi, December 2000.
LNCS 1974, pp.277289.
 M.
Hennessy, H. Lin and J. Rathke, Unique Fixpoint Induction for
MessagePassing Process Calculi. Science of Computer Programming
41(3), 241275 (2001). Elsevier.
 H.
Lin, Model Checking Valuepassing Processes. 8th AsiaPacific
Software Engineering Conference (APSEC'2001), Macau, December 47,
2001. [paper.ps.gz]
 A.
Ingolfsdottir and H. Lin, A Symbolic
Approach to Valuepassing Processes. Chapter 7 of Handbook of
Processes Algebra. Elsevier. 2001. [paper.ps.gz]
 H.
Lin and Wang Yi, A Proof System for
Timed Automata. FOSSACS'2000, Berlin, March/April 2000. LNCS
1784, pp.208222. [paper.ps.gz]
 H.
Lin, Computing Bisimulations for FiniteControl piCalculus. Journal
of Computer Science and Technology, Vol.15, No. 1, 2000. [paper.ps.gz]
 H.
Lin, Inference Systems for Observation Equivalences in the piCalculus
(in Chinese). Science in China (Series E), Vol.29, No.5,
pp.452463. 1999.
 H.
Lin, "Onthefly" Instantiation of Valuepassing Processes.
FORTE/PSTV'98, Paris, November 1998. pp. 215230. Kluwer Academic
Publishers. [paper.ps.gz]
 H.
Lin, Complete Proof Systems for Observation Congruence in
FiniteControl piCalculus. ICALP'98, Aalborg, Denmark, August
1998, pp. 443454. LNCS 1443. Springer. [paper.ps.gz]
 M.
Hennessy and H. Lin, Unique Fixpoint Induction for Message passing
Process Calculi. CATS'97, Sydney, Australia, Feb. 1997, pp.
122131. [paper.ps.gz]
 H.
Lin, On Removing Unguarded Recursions in The piCalculus (in Chinese).
Journal of Software. Vol. 8, pp. 321326. 1997.
 M.
Hennessy and H. Lin, Proof Systems for Messagepassing Process Algebras.
Formal Aspects of Computing, Vol. 8, pp. 379407. 1996. Springer. [paper.ps.gz]
 H.
Lin, Symbolic Transition Graph with Assignment. CONCUR'96,
Pisa, Italy, August 1996. pp. 5065. LNCS 1119. [paper.ps.gz]
 H.
Lin, PAM: A Process Algebra Manipulator. Formal Method in
Systems Design, Vol. 7, No. 3, pp. 243259, 1995. Kluwer Academic
Publishers. [paper.ps.gz] An extended abstract of
this paper appeared in CAV'91, Aalborg, Denmark, July 1991. LNCS
575. pp. 136146.
 M.
Hennessy and H. Lin, Symbolic Bisimulations. Theoretical
Computer Science, Vol. 138, pp. 353  389, 1995. Elsevier.
 H.
Lin, Unique Fixpoint Induction for Mobile Processes. CONCUR'95,
Philadelphia, USA, August 1995, pp. 88102. LNCS 962. [paper.ps.gz]
 H.
Lin, On Implementing Unique Fixpoint Induction for Valuepassing Processes.
TACAS'95, Aarhus, Denmark, May 1995. [paper.ps.gz]
 H.
Lin, Proof Systems for the piCalculus (in Chinese). Advances in
Theoretical Computer Science, Nov 1994. pp. 15.
 H.
Lin, Symbolic Bisimulations and Proof Systems for the PiCalculus. Sussex University Computer Science
Report 1994:07. [paper.pdf]
 H.
Lin, Procedural Implementation of Algebraic Specifications. ACM
Transactions on Programming Languages and Systems, Vol. 15 No. 5, pp.
876895, 1993. ACM Press.
 H.
Lin, A Verification Tool for
ValuePassing Processes. 13th IFIP Symposium on Protocol
Specification, Testing and Verification, Liege, Belgium, May 1993. pp.
7992. NorthHolland. [paper.ps.gz]
 H.
Lin, An Interactive Proof Tool for
Process Algebras. 9th Symposium on Theoretical Aspects of Computer
Science, Paris, Feb. 1992. LNCS 577.
 H.
Lin and M.C. Pong, Modeling Multiple Inheritance
with Colimits. Formal Aspects of Computing, Vol. 2 No.4, pp.
301311, 1990. Springer.