大學教授
1985年至1988年於北京師範大學數學系，師從王世強，主攻模型論。獲博士學位；1989年至1991年獲Volkswagen Stiftung在聯邦德國Freiburg 大學邏輯研究所作博士後的研究，師從H.-D.Ebbinghaus,學習模型論邏輯與有限模型論。1993年底進入上海交通大學計算機系，工作至今。
曾主持二項國家自然科學基金項目：“分劃邏輯在計算機科學中的套用”，1995年至1997年，1998年結題時被基金委信息學部專家組評為特優項目；“一類新的時態邏輯框架”，1997年至1999年。
發表文章
Z-自動機與分劃邏輯，數學學報 Vol.41 No.1 (1998) (與別榮芳合作)
有限狀態可識別性與分劃邏輯，《國家自然科學基金資助項目研究成果年報》信息科學專輯，（1998）
大小EC結構的可判定性，數學學報，40（1997），No.3.
模型論邏輯與理論計算機科學，數學進展，24（1996）， No.3.
命題時態邏輯的分劃式擴充，軟體學報 vol.7 (1996)（增刊）.
L(P1,1)和正則語言，計算機學報 19（1996）,No.11. (與田啟家，史忠植合作)
分劃邏輯與著色卵石博弈 數學進展，24 (1995) No.6
分劃邏輯與樹型自動機 in《理論計算機科學進展》陳火旺等編（1994）
分劃邏輯與傳遞閉包邏輯，科學通報，38（1993），No.14.
The decidability of finite forcing companion. Chinese Ann. of Pure & appl. Logic,2 (1992).
一類具有量詞消去性質的偏序結構，科學通報 37（1992）No.23
有限力迫伴隨的可判定性,科學通報，35（1990），No.15.
有限弱力迫的布爾值模型表示，北師大學報 （1990）No.3
