Kai Lin

Links    Kumo Documentation    Hidden algebra    The BOBJ languages

Publications Web-based Multimedia Support for Distributed Cooperative Software Engineering, by Joseph Goguen and Kai Lin, in Proceedings, International Symposium on Multimedia Software Engineering, (Taiwan) December 2000, IEEE Press, pages 25-32. Overview of the Tatami project and the Kumo website editor and proof assistant, focusing on design decisions and use of the web; describes how Kumo integrates formal and informal methods for software development, in a distributed cooperative environment. Behavioral and Coinductive Rewriting, by Joseph Goguen, Kai Lin, and Grigore Rosu. Keynote address, in Proceedings, Rewriting Logic Workshop, 2000, edited by Kokichi Futatsugi, Japan Advanced Institute of Science and Technology, September 2000, pages 1-22. A somewhat informal summary of recent results on simulating behavioral rewriting with standard rewriting, and on circular coinductive rewriting; the latter is a surprisingly effective algorithm for proving behavioral equalities. An Overview of the Tatami Project, by Joseph Goguen, Kai Lin, Grigore Rosu, Akira Mori and Bogdan Warinschi, in Cafe: An Industrial-Strength Algebraic Formal Method, edited by Kokichi Futatsugi, Tetsuo Tamai and Ataru Nakagawa, Elsevier, 2000, pages 61-78. This is a high level snapshop of the UCSD Tatami project as of late 1999. Tools for Distributed Cooperative Engineering, by Joseph Goguen, Kai Lin, Akira Mori and Grigore Rosu. Describes how the Kumo website editor/proof assistant integrates formal and informal methods for software development, in a distributed cooperative environment. A verification step can be the scan of an envelope back, a diagram or applet, as well as a fully formal subproof. In Proceedings, CafeOBJ Symposium (26-29 April 1998, Kyoto, Japan). Distributed Cooperative Formal Methods Tools, by Joseph Goguen, Kai Lin, Akira Mori, Grigore Rosu and Akiyoshi Sato. Overview of Tatami project tools and methods, including hidden algebra and algebraic semiotics, with examples. Proceedings, Automated Software Engineering (Lake Tahoe NV, 3-5 Nov 1997) IEEE, pages 55-62. Algebraic Semiotics, ProofWebs and Distributed Cooperative Proving, by Joseph Goguen, Akira Mori and Kai Lin. Describes the ProofWeb data structure and the Kumo proof assistant and website generator system, plus methods from semiotics used in their design, with examples. In Proceedings, User Interfaces for Theorem Provers (Sophia Antipolis, France, 1-2 Sept 1997) pages 25-34. Personal Information I got Master Degree from Shanghai Jiao Tong University. My hometown is Shanghai, the biggest city in China. I expect to finish my study in UCSD by July, 2001. Now I am looking for a job in software development.