报告时间：2021年3月19日 （周五） 15:30 – 17:30
地点： 北京大学理科一号楼1501
线上会议：腾讯会议 324 396 128
Title: Constructive Bidirectional Programming
Presenter: Zhenjiang Hu (Peking University)
Abstract: Bidirectional Transformation provides a powerful mechanism for synchronizing and maintaining the consistency of information between different representations. Although many languages have been proposed to support programming bidirectional transformations, we are lacking systematic ways to develop both correct and efficient bidirectional transformation. In this talk, we show that the program calculation technique, which is known to be useful for development of unidirectional functional programs, is useful for systematic development of correct and efficient bidirectional functional programs from a straightforward specification through correctness-preserving calculation.
Bio: Zhenjiang Hu is Chair Professor in Department of Computer Science and Technology, Peking University. He received his B.S. and M.S. degrees from Shanghai Jiao Tong University in 1988 and 1991, respectively, and Ph.D. degree from University of Tokyo in 1996. He was a lecturer (1997–2000) and an associate professor (2000–2008) in University of Tokyo, a full professor at NII (2008-2019), and a full professor at University of Tokyo (2018-2019), before joining Peking University in 2019. His main research interest is in programming languages and software engineering in general, and functional programming, parallel programming, and bidirectional programming in particular. He is Fellow of JFES (Japan Federation of Engineering Society), Fellow of IEEE, Member of Academy of Europe, and Member of Engineering Academy of Japan.
Title: Type-based Language Design
Presenter: Ningning Xie (University of Hong Kong)
Abstract: In recent years, programming language design is more active than ever. Existing languages have seen a dramatic surge of new features that significantly extends the their expressive power, and numerous new languages are being actively developed. Unfortunately, without careful formalization, programming languages can be bogus, which in turn leads to ad-hoc fixes and solutions. My work tackles this challenge by applying theoretical rigor to design reliable and scalable programming languages, such that existing as well as new language features can be reasoned in a precise manner from first principles. As an example, I will describe the design of the kind inference algorithm for the Haskell programming language. This work provides type-theoretic formalization of the algorithm, which establishes desirable language properties and guides the continued evolution of language implementations. In the second part, I will show how to support computational effects through formal type and effect systems in the Koka programming language, such that side-effects of programs can be reasoned and their implementations are guaranteed to be efficient.
Bio: Ningning Xie is a PhD candidate at the Programming Languages Group at the University of Hong Kong. Prior to graduate school, she received her B.S. degree in Computer Science from Zhejiang University. Her research interests are in the field of programming languages, focusing on functional programming and type theory. During her Ph.D study, Ningning was an intern at Microsoft Research Redmond. She is a recipient of the ACM SIGPLAN Distinguished Paper Award at the Symposium on Principles of Programming Languages (POPL 2020), and was selected for Rising Stars 2020 organized by UC Berkeley.
