My name is Andrey Yao. I am passionate about software verification and formal methods. In the age of LLM assistance, I find it increasingly important to ensure that the efficiency of software development does not come at the cost of correctness.
I recently finished my MS in computer science at the University of Wisconsin-Madison. I worked with professor Ethan Cecchetti on various projects in programming language theory. I designed language semantics and type systems for choreographic programming, an emergent paradigm for distributed computing that combines interactions between different hosts into a single program. I also developed a formal semantics and type-and-effect system for a Haskell-like language with lazy semantics, which mathematically guarantees a security property called noninterference. Some of my work also included formalization of definitions and theorems in proof assistants such as Rocq.
Before UW-Madison, I earned my bachelor's degree in computer science and mathematics at Cornell University.
I am currently actively looking for work!