HomeDate: 2024-03-18
Dr. Liang-Ting Chen earned his Ph.D. in Computer Science from the University of Birmingham in the UK under the supervision of Achim Jung, where he studied the intersection of modal logic and coalgebra and developed the mathematical structure of coalgebraic modalities. He joined the Institute of Information Science, Academia Sinica as an Assistant Research Fellow in October, 2023. Prior to Academia Sinica, he held postdoctoral fellowships at TU Braunschweig (Germany), University of Hawaii at Manoa (USA), Swansea University (UK), Academia Sinica (Taiwan) on diverse topics, contributing to the fields of algebraic automata theory, category theory, type theory, and dependently typed programming.
With an interest in mathematical structures within computer science, Dr. Chen’s focus lies in exploring the realms of 'theory B' in theoretical computer science. In recent years, he has been exploiting the computational and logical aspects of type theory, particularly through the lens of the Curry-Howard correspondence. He has made contributions to both the theoretical underpinnings and practical applications of programming languages, using Agda, a proof assistant, and a dependently typed language. One of recent contributions is the formal development of a mathematical theory of bidirectional typing, which can be viewed as a verified implementation of a type-synthesiser generator for a class of programming languages. This work demonstrates the practical utility of type theory and highlights Dr. Chen's vision of unifying programming language theory and implementation.
