September 14, 2023
Embedding describes the process of encoding a program’s syntax and/or semantics in another language—typically a theorem prover in the context of mechanized reasoning. Among different embedding styles, deep embeddings are generally preferred as they enable the most faithful modeling of the original language. However, deep embeddings are also the most complex, and working with them requires additional effort. In light of that, this talk aims to draw more attention to “shallower” styles, namely shallow and mixed embeddings, by studying their use in mechanized reasoning. More specifically, I present a simple shallow embedding for reasoning about computation costs of lazy programs, and a class of mixed embeddings that are useful for reasoning about properties of general computation patterns in effectful programs.
About Yao Li
Yao Li (He/Him) is an assistant professor of computer science at Portland State University. His main research area is in functional programming, interactive theorem proving, and program verification. His current research focuses on using interactive theorem provers to verify existing programs written without verification in mind. Some of his past work includes the verification of the DeepSpec web server and the verification of Haskell’s containers library (using hs-to-coq). He obtained his Ph.D. from the University of Pennsylvania in 2022, under the supervision of Stephanie Weirich. Before that, he obtained a MS degree and a BS degree from Shanghai Jiao Tong University in 2016 and 2013, respectively.