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 Universtion 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 postdocs
I have some funding available to hire a self-motivated postdoc 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.
兼任助理
初步以背景知識研習為主，同時使用定理證明系統 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.