首頁發布時間: 2024-03-18
陳亮廷博士在教授Achim Jung指導下於英國伯明翰大學取得電腦科學博士學位，博士論文主題是模態邏輯和共代數（coalgebra）的交叉領域，主要探討共代數模態邏輯（coalgebraic modal logic）的數學結構。後曾於德國不倫瑞克工業大學、美國夏威夷大學馬諾阿分校、英國斯旺西大學以及本院進行博士後研究，研究主題涵蓋了代數自動機理論、範疇論（category theory）、型別論（type theory）以及依值型別程式設計（depenently typed programming）等領域。於2023年10月加入本院資訊科學研究所擔任助理研究員。
陳博士對電腦科學中的數學結構極感興趣，其研究主要集中在探索理論電腦科學中的「理論B」領域。近年來，陳博士利用型別理論的計算面和邏輯面使用Agda作為證明證明和依值型別程式語言，發展程式語言設計的理論而數學證明又可作為保證為正確的軟體實作。例如：近來發展雙向類型（bidirectional typing）的型式化數學理論，除了抽象理論刻畫一整類程式語言外，該理論可同時作為適用於的型別檢查與合成（type synthesiser）的生成器實作。這項研究展示型別理論的實際應用價值，以及陳博士統一數學理論與實作兩者相結合的願景。
ｘ快問快答ｘ
Q. 用一句話形容自己的研究？
A. 用邏輯語言描述「計算」與「程式語言」的數學結構。
Q. 若請您寫一段話掛在實驗室／研究室牆上，會寫些什麼？為什麼？
A. “Get your hands dirty.” 因為即便是理論研究，也不能只跟隨文獻中前人發展出來的研究成果，而是得從問題發想到定理證明都需要從各種角度反覆推敲，嘗試不同的數學定義到思考實際的可能用途與影響，嘗試從雜亂尚未有清楚定義的問題中梳理開拓新的研究路線。
