Chen, Liang-Ting 陳亮廷

Profile Photo

✉️ ltchen@iis.sinica.edu.tw

Assistant Research Fellow (Assistant Professor)
Institute of Information Science
Academia Sinica, Taiwan

🧑🏻‍🔬 About Me

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

I have a double major in Mathematics and Computer Science from the National Cheng Kung University, Taiwan. I earned my PhD in Computer Science at the University of Birmingham, the UK, under the supervision of Achim Jung. Following my PhD, I worked as a postdoc in Germany, the USA, and the UK.

🫵🏼 Hiring 徵才啟事 🫵🏼

有興趣探索「程式語言」或「型別論」的學生，歡迎寄信給我詳談細節。

Prospective research assistants
I have some funding available to hire self-motivated research assistants to join me at Academia Sinica. If you are interested in the research topics of my recent work, please feel free to drop me an email with a brief statement and your résumé to initiate a conversation.

Please note that, due to current geopolitical circumstances, only short-term student visits can be accommodated for Chinese applicants.

兼任助理
初步以背景知識研習為主，同時使用定理證明系統 Agda 加強數學論證能力及實作能力，逐步發展研究題目。
暑期實習生
在兩個月間，參加相關暑期課程，從實習生自己的興趣發展可用 Agda 形式化的問題，藉此學習此領域的知識跟原則，判斷是否適合進一步發展。

📜 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 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.

🧑‍🏫 Supervision

Past
Summer interns
  • Yu-Chuan Yu 游棫荃, Bridging Combinatorial and Algebraic proof: An Algebraic Approach with Agda (abstract), 2024
  • Chih-Hsiang Chuang 莊智翔, Circuit Realization of Truth Tables and Boolean Functions in Agda (abstract), 2024
  • Ting-Wu Chang 張庭梧, Constructions and Properties of the Heighway Dragon Curve Formalized in Agda (abstract), 2024
  • Wen Chun Kao 高文君, Verification of Correctness and Time Complexity of Skew Binomial Heap via CALF (abstract), 2024

🏅 Award

  • EATCS Best Paper Award at the 42nd International Symposium on Mathematical Foundations of Computer Science, 2017

  • PhD Studentship from the UK EPSRC Project Coalgebraic Logic—Extending the Scope, 2009

🎤 Invited Talk

  • From Datatype Genericity to Language Genericity
    WG6 Meeting of European Research Network on Formal Proofs, Leuven, Belgium, 2024
  • Foundations of Mathematics, Topoi, and Functional Programming Languages
    Math Club, Department of Mathematics, National Taiwan University, Taiwan, 2023

💰 Funding

  • 2025–2027, Principal investigator, Theory, Applications, and Implementation of Inductive Types, funded by NSTC (114-2222-E-001-001-MY3, TWD$2,181,000)
  • 2020–2023, Unnamed, Type-theoretic foundations for metaprogramming, funded by NSTC (109-2222-E-001-002-MY3, TWD$2,851,000, PI: Hsiang-Shang Ko)

🛠️ Service

PC Membership

2026
  • European Symposium on Programming (ESOP)
2025
  • International Conference on Types for Proofs and Programs (TYPES)
  • ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM)
2024
  • ACM Student Research Competition (SRC) at ICFP
  • ACM SIGPLAN Haskell Symposium
  • Workshop on Mathematically Structured Functional Programming (MSFP)
  • SRC at Asian Symposium on Programming Languages and Systems (APLAS)
2023
  • ACM SIGPLAN International Conference on Functional Programming
2021
  • Workshop on Type-Driven Development (TyDe)

Organising

  • Formosan Summer School on Logic, Language, and Computation (FLOLAC)
    Co-organiser (2024, 2022, 2020, 2018) with Hsiang-Shang Ko, Lecturer (2024, 2022, 2020, 2018, 2016, 2014)
  • Agda Implementors’ Meeting XXXVII (AIM XXXVII)
    Local organiser

External Review

ICFP’24, CPP’24, PPDP’20, CONCUR’20, POPL’18, SAC’18, CALCO’17, LICS’17, LICS’16, PODS’16, LICS’15, MPC’10, ICFP’09

✍🏼 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.