Yifei Sun

I am a PhD student at ENS de Lyon Avalon Team and Inria DataMove Team co-supervised under Olivier Richard and Christian Perez. I got my master's from Northeastern University advised by Ji-Yong Shin at Systems Research Group. I was a research intern advised by Tomoharu Ugawa at University of Tokyo Computing Software Group. I finished my undergrad at University of Utah advised under Shad Roundy and Tucker Hermans.

I'm generally interested in systems and theory (CV), topics include:

• Reproducible HPC testbed infrastructure, experiment description, configuration and reconfiguration formalization, and programmable networking via eBPF/XDP
• Formal verification of consistency and safety properties in distributed systems
• Constructive type theory and mechanized proofs

My contact info is hidden within the source code of this site. Search for the platform you want to reach me on in all lowercase (e.g. github, linkedin, etc.). You can reach me directly with Matrix, Discord (use my GitHub username), or email (echo -n 'eXN1bkBoZXkuY29tCg==' | base64 --decode).

I daily drive a Framework Laptop 13 with NixOS and a 14-inch MacBook Pro with nix-darwin on the go. I own and operate AS10779 and AS18932 (PeeringDB, looking glass). I maintain about 300 packages and quite actively contribute to the Nix ecosystem. During my free time, I enjoy writing weird code nobody uses (daily), swimming (sometimes, but I used to swim competitively), and playing osu! (mostly std on a Wacom Intuos Pro originally bought for a digital art class). Streaming services? Apple Music all the way (playlist)!

Turns out .arpa zones can serve HTTP (tried HTTPS but CAs won't issue for .arpa) and many more ;) Who knew:

• http://0.0.9.5.f.2.0.6.2.ip6.arpa
• http://104.161.23.in-addr.arpa
• http://136.104.192.in-addr.arpa

Random recommendations:

• Paid search engine Kagi, you control the ranking
• NixOS for your next OS
• Self-hostable code search engine Zoekt
• Get an amateur radio license, my callsign is KC1VZR
• Email over radio with Winlink + Pat
• Tailscale, Headscale, or at least WireGuard
• Kanidm for OAuth/OIDC and read-only LDAP
• Your PL journey should start with OCaml and Dune is pretty good
• Write a toy language?
• Learn how to mechanize proofs?
• Cobalt, yet another online FFmpeg wrapper, but nice
• Cloudflare's public RTR server for route filtering
• Secure NTP with ntpd-rs NTS
• Tailscale doesn't cut it? Try ranet IPsec full mesh

Huge thanks to the following sponsors! They were warned (or not?) and chose to proceed anyway ;)