I am going to join the
Computer Science Department of
Portland State University as tenure-track assistant professor this fall!
I am looking for students! Feel free to contact me (my email can be found above) if you are interested in programming languages/formal verification/interactive theorem proving.
You can find more about my research interests from my publications (listed below).
- Reasoning about the Garden of Forking Paths
by Yao Li, Li-yao Xia, Stephanie Weirich
the ACM SIGPLAN International Conference on Functional Programming (ICFP), 2021
Talk
Paper (Open access)
Artifact
- Verifying an HTTP Key-Value Server with Interaction Trees and VST
by Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, Steve Zdancewic
12th International Conference on Interactive Theorem Proving (ITP), 2021
Paper (open access)
Artifact
- Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language
by Jay Bosamiya, Sydney Gibson, Yao Li, Bryan Parno, Chris Hawblitzel
12th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2020
Paper
Pre-print
- A Scala based Framework for Developing Acceleration Systems with FPGAs
by Yanqiang Liu, Yao Li, Zhengwei Qi, Haibing Guan
Journal of Systems Architecture, Volume 98, 2019
Paper
- From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
by Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic
8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), 2019
Paper (public access)
- Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code (Experience Report)
by Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Stephanie Weirich
the ACM SIGPLAN International Conference on Functional Programming (ICFP), 2018
Talk
Paper (open access)
Journal Version
Journal Pre-print
Artifact
- AutoBench: Finding Workloads That You Need Using Pluggable Hybrid Analyses
by Yudi Zheng, Andrea Rosa, Luca Salucci, Yao Li, Haiyang Sun, Omar Javed, Lubomír Bulej, Lydia Y. Chen, Zhengwei Qi, Walter Binder
23rd IEEE International Conference on Software Analysis, Evolution, and Reengineering (SANER), 2016
Paper
- ScalaHDL: Express and Test Hardware Designs in a Scala DSL
by Yao Li, Antonio R. Lopes, Zhouyun Xu, Zhengwei Qi, Haibing Guan,
32nd IEEE International Conference on Computer Design (ICCD), 2014
Paper
- The Expression Problem and Theorem Proving (Discussion)
Workshop on the Implementation of Type Systems (WITS), co-located with POPL, Philadelphia, PA, 2022
- Effect-Oblivious Equivalence
Workshop on Principles of Secure Compilation (PriSC), co-located with POPL, Philadelphia, PA, 2022
- Reasoning about the Garden of Forking Paths
POPV seminar at Boston University (Longer Version, Invited Talk), 2021
The ACM SIGPLAN International Conference on Functional Programming (ICFP), virtual talk, 2021
The ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH), Chicago, IL, 2021
- Embracing a Mechanized Formalization Gap: Interactive reasoning for Haskell at scale
Haskell Implementors’ Workshop (HIW), co-located with ICFP, virtual talk, 2020
- The Science of Deep Specification
NSF Expeditions in Computing - 10 Years of Transforming Science and Society, Washington, DC, 2018
- Dependent Types in Scala
Philly Area Scala Enthusiasts Meetup (PHASE), Philadelphia, PA, 2017
- Scala-Forklift: Type-Safe Data Migration Tool for Slick, Git and Beyond
Comcast Scala By the Schuyllkill Conference, Philadelphia, PA, 2017
- Teaching Assistant: Theory of Computation (University of Pensylvania), 2018 Spring
- Teaching Assistant: Advanced Programming (University of Pennsylvania), 2017 Fall
- Teaching Assistant: Programming and Data Structures II (Shanghai Jiao Tong University), 2013 Fall
- Research Intern at Microsoft
Jun. 2018 - Aug. 2018, Redmond, WA, USA
Vale Project, under supervision of Chris Hawblitzel
- Visiting Researcher at University of Lugano
Mar. 2015 - Jun. 2015, Lugano, Ticino, Switzerland
Dynamic Analysis Group, under supervision of Walter Binder
- Software Development Engineer Intern at Microsoft
Jun. 2012 - Sep. 2012, Shanghai, China
Infrastructure team, under supervision of Zhiliang Xu
- Artifact Evaluation Committee: POPL'22, ICFP'21, POPL'21
- Session Chair: SPLASH'21
- Mentor: DeepSpec REU'21 (UPenn), Google Summer of Code (Scala) 2016
- Student Volunteer Co-Chair: SPLASH'22
- Student Volunteer: ICFP'21, ICFP'20, DeepSpec Summer School'17
- Google Open Source Peer Bonus (for Scala Forklift), 2018
- Outstanding Graduate of Shanghai Jiao Tong University, 2016
- China National Scholarship, 2014
- Outstanding Graduate of Shanghai Jiao Tong University, 2013
- China National Scholarship, 2012
- Most Popular Collegiate Innovation Projects of Shanghai Jiao Tong University, 2012
- 1st Prize in the 4th Intel Cup National Collegiate Software Innovation Contest in China, 2011
- 1st Prize in National Olympiad in Informatics in Provinces, 2008
- 1st Prize in National Olympiad in Informatics in Provinces, 2007
- Puzzles, escape rooms, board games
- Still learning: fencing, archery