Dr. Zhenyu Qian

(former member of Kestrel's research staff)


I have been with Kestrel Institute since April 1998. Prior to joining Kestrel, I held academic positions at Bremen University in Germany, where I received my Ph.D. degree and "Habilitation" in Computer Science in 1991 and 1996, respectively.

Research Interests

Java-based internet security, Java extensions, Java semantics, distributed computing, Jini, object-oriented, functional, concurrent, logic programming languages, specification languages, compiler construction, program specification, program construction, program transformation, object-oriented analyse and design, types, lambda-calculus, unification, algebraic semantics, theorem proving systems.

Research Projects



Conferences and chapters in books

  • Zhenyu Qian, Allen Goldberg and Alessandro Goglio. A Formal Specification of Java Class Loading, to appear in Proc. ACM Conf. on Object-Oriented Programming, Systems, Languages, and Applications, 2000.
  • Alessandro Coglio, Allen Goldberg and Zhenyu Qian. Towards a Provably-correct Implementation of the JVM Bytecode Verifier. In Proc. DARPA Information Survivability Conference and Exposition (DISCEX'00), Vol. 2, pages 403-410, IEEE Computer Society, 2000.
  • Zhenyu Qian. A Formal Specification of Java(tm) Virtual Machine Instructions for Objects, Methods and Subroutines, in Jim Alves-Foss (ed.) "Formal Syntax and Semantics of Java(tm)", Springer Verlag LNCS 1523, 1998.
  • Zhenyu Qian and Besma AbdMoulah. Entwurf und prototypische Implementierung einer objektorientierten funktionalen Programmiersprache. Im Tagungsband der GI-Jahrestagung 1997, ``Informatik Aktuell'', Springer Verlag, 1997.
  • Zhenyu Qian and Bernd Krieg-Brückner. Typed Object-Oriented Programming with Late Binding. In Proc. 10th European Conf. on Object-Oriented Programming, Springer-Verlag LNCS, pages 48-72, 1996.
  • Zhenyu Qian and Bernd Krieg-Brückner. Object-Oriented Functional Programming and Type Reconstruction. In M. Haveraaen and O. Owe and O.-J. Dahl, editors, Recent Trends in Data Type Specification, Springer-Verlag LNCS 1103, pages 458-477, 1996.
  • Regis Curien, Zhenyu Qian and Hui Shi. Efficient Second-Order Matching. In Proc. 7th Int. Conf. Rewriting Techniques and Applications, Springer-Verlag LNCS 1103, pages 317-331, 1996.
  • Zhenyu Qian and Bernd Krieg-Brückner. An approach to object-oriented functional programming. In A. Pnueli and H. Lin, editors, Proc. 1995 Int. Workshop on Logic and Software Engineering, World Scientific Publ., pages 71-89, 1996.
  • Jun Liu and Zhenyu Qian. Using first-order narrowing to solve goals of higher-order patterns. In M. Takeichi and T. Ida, editors, Proc. Fuji Int. Workshop on Functional and Logic Programming, World Scientific Publ., pages 134-147, 1995.
  • Zhenyu Qian. Higher-order equational logic programming. In Proc. 21st ACM Symp. Principles of Programming Languages, pages 254-267, 1994.
  • Zhenyu Qian and Kang Wang. Modular AC unification of higher-order patterns. In J.-P. Jouannaud, editor, Proc. Int. Conf. on Constraints in Computational Logics, Springer-Verlag LNCS 845, pages 105-120, 1994.
  • Zhenyu Qian. Linear unification of higher-order patterns. In M.-C. Gaudel and J.-P. Jouannaud, editors, Proc. Theory and Practice of Software Development, LNCS 668, pages 391-405, 1993.
  • Zhenyu Qian and Kang Wang. Higher-order E-unification for arbitrary theories. In K. Apt, editor, Proc. 1992 Joint Int. Conf. and Symp. on Logic Programming, MIT Press, pages 52-66, 1992.
  • Tobias Nipkow and Zhenyu Qian. Reduction and unification in lambda calculi with subtypes. In D. Kapur, editor, Proc. 11th Int. Conf. Automated Deduction, LNCS 607, pages 66-78, 1992.
  • Tobias Nipkow and Zhenyu Qian. Modular higher-order E-unification. In R.V. Book, editor, Proc. 4th Int. Conf. Rewriting Techniques and Applications, LNCS 488, pages 200-214, 1991.
  • Zhenyu Qian. Unification in combinations of second order types and linear shallow algebraic theories. In S. Kaplan and M. Okada, editors, Proc. 2nd International Workshop on Conditional and Typed Rewriting Systems, LNCS 516, pages 448-453, 1991.
  • Hans-Jörg Kreowski and Zhenyu Qian. Relation-sorted algebraic specifications with built-in coercers: Basic notions and results. In C. Choffrut and T. Lengauer, editors, Proc. 7th Symposium on Theoretical Aspects of Computer Science, LNCS 415, pages 165-176, 1990.
  • Zhenyu Qian. Higher-order order-sorted algebras. In H. Kirchner and W. Wechler, editors, Proc. 2th Int. Conf. Logic and Algebraic Programming, LNCS 463, pages 86-100, 1990.
  • Zhenyu Qian. Relation-sorted algebraic specifications with built-in coercers: Parameterization and parameter passing. In H. Ehrig, H. Herrlich, H.-J. Kreowski and G. Preu{\ss}, editors, Proc. Int. Conf. on Categorical Methods in Computer Science with Aspect from Topology, LNCS 393, pages 244-261, 1989.
  • Zhenyu Qian. Structured contextual rewriting. In P. Lescanne, editor, Proc. 2nd Int. Conf. on Rewriting Techniques and Applications, LNCS 256, pages 168-179, 1987.

Technical reports



  • Zhenyu Qian. Extensions of Order-Sorted Algebraic Specifications: Parameterization, Higher-Order Functions and Polymorphism. Universität Bremen, April 1991.

Edited Book

  1. Maura Cerioli, Martin Gogolla, Helene Kirchner,Bernd Krieg-Brückner, Zhenyu Qian and Markus Wolf (eds.): Algebraic System Specification and Development: Survey and Annotated Bibliography - Second Edition, June, 1997.


  1. Zhenyu Qian and Bernd Krieg-Brückner. COMPASS First Interim Report, 1993.
  2. Zhenyu Qian and Bernd Krieg-Brückner. COMPASS Second Interim Report, 1994