Liang-Ting Chen

Chen, Liang-Ting 陳亮廷

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.

Recent Posts

On vibe coding for the use of static website generators

March 29, 2026 Personal

🫵🏼 Hiring 徵才啟事 🫵🏼

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

Prospective research assistants: I have 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.

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

兼任助理: 初步以背景知識研習為主，同時使用定理證明系統 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.

🏅 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-Generic Programming to Language-Generic Programming
Workshop on Type-Driven Development (TyDe 2025), Singapore, Singapore, 2025
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)

🧑‍🏫 Supervision

Postdoc

Shu-Hung You 游書泓, 2025–

Recent Summer Interns

Yi-Ting Lo 羅翊庭, A Security Analysis of a Cryptographic Handshake Protocol (abstract), 2025
Anderson Wu 吳智堯, Propositions as Descriptions of Universes of Types and their Categorical Structures, 2025
Yu-Chuan Yu 游棫荃, Bridging Combinatorial and Algebraic proof: An Algebraic Approach with 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

PC Membership

2026

European Symposium on Programming (ESOP)
ACM SIGPLAN International Conference on Functional Programming (ICFP)

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