Rocqet makes it easier to build extensible trustworthy systems, like verified compilers, in Rocq.

Oghenevwogaga Ebresafe, Ian Zhao, Ende Jin, Arthur Bright, Charles Jian, Yizhou Zhang

Compiling high-level, modular algebraic effects to low-level, swift stack switching

Cong Ma, Zhaoyi Ge, Edward Lee, Yizhou Zhang

A compiler factorizes recursive probabilistic programs for scalable inference.

Jianlin Li, Eric Wang, Yizhou Zhang

Reconciling algebraic data types with scalable extensibility

Anastasiya Kravchuk-Kirilyuk, Gary Feng, Jonas Iskander, Yizhou Zhang, Nada Amin

An object-oriented idea lends itself to reusable proofs!

Ende Jin, Nada Amin, Yizhou Zhang

Symbolic methods (a type system and an analysis) aid in neural-network-based inference.

Jianlin Li, Leni Aniva, Pengyuan Shi, Yizhou Zhang

Reasoning principles for probabilistic programs that model rational agents

Yizhou Zhang, Nada Amin

Handlers for “effectful effects”? Yes, with a type system to defend abstractions.

Yizhou Zhang, Guido Salvaneschi, Andrew C. Myers

Robots plan paths against both noise and adversarial uncertainty.

Jacopo Banfi, Yizhou Zhang, G. Edward Suh, Andrew C. Myers, Mark Campbell

Algebraic effects (and hence exceptions, asynchrony, ...) made modular

Yizhou Zhang, Andrew C. Myers

A lot of polymorphism and extensibility in a lightweight package

Yizhou Zhang, Andrew C. Myers

The flexibility of unchecked exceptions, the static guarantees of checked exceptions, and good performance too

Yizhou Zhang, Guido Salvaneschi, Quinn Beightol, Barbara Liskov, Andrew C. Myers

An expressive, lightweight genericity mechanism with better code reuse and stronger static checking

Yizhou Zhang, Matthew C. Loring, Guido Salvaneschi, Barbara Liskov, Andrew C. Myers