Chen, Liang-Ting 陳亮廷

Assistant Research Fellow (Assistant Professor)

Institute of Information Science
Academia Sinica, Taiwan

ltchen@iis.sinica.edu.tw

About me

I am an assistant research fellow in the Theory Research Group at the Institute of Information Science, Academia Sinica in Taiwan.

Research Interests

I am generally interested in mathematical structures in computer science, specifically, the so-called ‘theory B’ of theoretical computer science. My work so far spans dependently typed programming, programming languages, logic, and automata theory, employing logical and categorical methods.

Recently, I have been exploring the computational and logical aspects of type theory, particularly through the lens of the lens of Curry-Howard correspondence. I have worked on both the theory and practice of programming languages using Agda, a proof assistant and a dependently typed language. This approach allows me to produce reliable, reproducible, and sometimes useful results.

Hiring 徵才啟事

兼任助理、暑期實習

歡迎有興趣探索「程式語言」以及「型別論」基礎的學生與我聯絡細節。

兼任助理初步會以補充背景知識，例如論文或教科書閱讀並定期報告、討論為主；同時使用定理證明系統 Agda 加強程式及數學論證能力，並動手嘗試不同作法，逐步發展可能的研究題目。若是暑期實習生則規劃在兩個月間，參加相關暑期課程，接著試著從相關學術興趣出發，發展一個符合程度且可用 Agda 形式化的問題開始，從研究中學習此領域的知識跟原則，藉此可判斷是否合適。

Prospective postdocs / research assistants

I have some funding available to hire a self-motivated postdoc and research assistants to join me at Academia Sinica.
If you find my work interesting to you, please feel free to send me an email with your résumé to initiate the conversation.

Academic service

Award

Invited Talk

Publications

(See also: DBLP or Google Scholar)

[1]
L.-T. Chen, H.-S. Ko, A formal treatment of bidirectional typing, in: S. Weirich (Ed.), 33rd European Symposium on Programming (ESOP), 2024. doi:10.1007/978-3-031-57262-3_5 (Slides).
[2]
H.-S. Ko, L.-T. Chen, T.-C. Lin, Datatype-generic programming meets elaborator reflection, in: 27th ACM SIGPLAN International Conference on Functional Programming (ICFP), 2022. doi:10.1145/3547629.
[3]
L.-T. Chen, H.-S. Ko, Realising intensional S4 and GL modalities, in: F. Manea, A. Simpson (Eds.), 30th EACSL Annual Conference on Computer Science Logic (CSL), Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2022. doi:10.4230/LIPIcs.CSL.2022.14.
[4]
J. Adámek, L.-T. Chen, S. Milius, H. Urbat, Reiterman’s theorem on finite algebras for a monad, ACM Transactions on Computational Logic. 22 (2021). doi:10.1145/3464691.
[5]
L.-T. Chen, M. Roggenbach, J.V. Tucker, An algebraic theory for data linkage, in: I. Fiadeiro, José Luiz and Ţuţu (Ed.), 24th IFIP WG 1.3 International Workshop on Algebraic Development Techniques (WADT’18), Springer, 2019. doi:10.1007/978-3-030-23220-7_3.
[6]
H. Urbat, J. Adámek, L.-T. Chen, S. Milius, Eilenberg theorems for free, in: K.G. Larsen, H.L. Bodlaender, J.-F. Raskin (Eds.), 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2017. doi:10.4230/LIPIcs.MFCS.2017.43.
[7]
L.-T. Chen, H. Urbat, Schützenberger products in a category, in: S. Brlek, C. Reutenauer (Eds.), 20th International Conference on Developments in Language Theory (DLT), Springer Berlin Heidelberg, 2016. doi:10.1007/978-3-662-53132-7_8.
[8]
L.-T. Chen, J. Adámek, S. Milius, H. Urbat, Profinite monads, profinite equations, and Reiterman’s theorem, in: B. Jacobs, C. Löding (Eds.), 19th International Conference on the Foundations of Software Sciences and Computer Structures (FoSSaCS), Springer Berlin Heidelberg, 2016. doi:10.1007/978-3-662-49630-5_31.
[9]
L.-T. Chen, H. Urbat, A fibrational approach to automata theory, in: L.S. Moss, P. Sobocinski (Eds.), 6th Conference on Algebra and Coalgebra in Computer Science (CALCO), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2015. doi:10.4230/LIPIcs.CALCO.2015.50.
[10]
L.-T. Chen, A. Jung, On a categorical framework for coalgebraic modal logic, in: 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS), Elsevier, 2014. doi:10.1016/j.entcs.2014.10.007.