我的主要研究興趣包括程式語言與函數語言，尤其是代數式、關係式的程式推導。細目包括:

        程式推導： 由系統規格推演出程式的方法。通常我們把系統規格寫成一個二元關係（binary relation），然後經過一系列的推演，轉化成一個函數語言程式。如此產生出的程式可確保是正確的。我同時也對使用最弱初使條件（weakest precondition）的程序式語言程式推導有興趣。反函數：許多問題都能描述成尋找某些常見函數的反函 數。我的早期研究提及如何將一個函數的反函數描述成一個「摺（fold）」。我們同時也在研究如和把反函數應用在 XML 編輯與處理之上。

        雙向更新：假設有一些原始資料，經過某函數轉換成另一種可顯示給使用者看的資料結構。使用者可修改、編輯之。「雙向更新」問題則是如何把使用者的編輯動作反映到原始資料上。我在東京大學的研究即嘗試運用反函數處理雙向更新問題。

        依存型態：近代程式語言使用表達力高的型態系統確保一些可由編譯器驗證的性質。依存型態（dependent types）是一種表達力極高的型態系統。近年來，許多學者投入其相關研究。我對如何把依存型態融入實用的程式設計感到有興趣。