Institute of Information Science, Academia Sinica

In various problem domains, there is always a need for languages that offer a convenient way to express computation and properties specific to their respective domains. For example, SQL is widely used for managing relational databases, WebAssembly is employed for low-level but memory-safe programming, and Dafny is utilised for program verification, with each language tailored to its own domain with specific features. As new domains continue to emerge and the need for domain-specific languages persists, a theory of language design is needed to deal effectively with the evolving landscape of languages.
Language design encompasses not only the syntax but also the semantics of programming languages, including how programs should be executed and their meta-properties (for example, every program in WebAssembly is guaranteed to be memory-safe, preventing code from accessing user or system memory). Rigorously proving that a language achieves its claimed meta-properties requires a formal definition of the language. However, formal definitions are inherently complex, as are the proofs of their meta-properties. As a result, programming language theorists often focus on developing minimalistic languages that are manageable, rather than attempting to model the intricacies of real-world languages. Furthermore, each language and its meta-properties are typically designed and proved from scratch, without the ability to reuse the results from smaller languages directly. This lack of scalability poses challenges for current methodologies in language design when it comes to real-world languages.
In my research, I have aimed for a novel approach to language design that leverages universal algebraic theories using category theory. This approach enhances the modularity and reusability of language design, enabling the development of more sophisticated languages for practical use cases. I have worked on combining individual modalities for state-based transition systems into a single logical system, and studied a universal theory for profinite algebras to specify sets of strings accepted by variants of finite state automata. Recently I am working on a universal algebraic theory of languages that can be defined inductively, spanning from binary trees to typed functional languages, and can be used for actual programming tasks and designing new languages in a modular manner. I will also emphasise the potential impact of my research on language design, including its implications for improving the scalability, modularity, and reusability in language design.

Dr. Liang-Ting Chen holds a PhD in Computer Science from the University of Birmingham, UK, with expertise in category theory and theoretical computer science. He has held postdoctoral positions in Germany, the UK, and Taiwan, and has made contributions to research areas including universal algebra, logic, automata theory, and programming languages. Dr. Chen's achievements include receiving a Best Paper Award from the European Association for Theoretical Computer Science for his work on unifying Eilenberg correspondences in automata theory, as well as contributions to the proof assistant Agda as a member of the development team. He has published papers in well-established conferences and journals such as ICFP, ToCL, MFCS, FoSSaCS, CSL, and DLT, and has collaborated with esteemed scholars in the field.