Michael Lan

I am a student at UCLA, where I am currently pursuing my bachelor's in computer science along with a minor in philosophy. Although I'm not actively conducting research at present, I enjoy thinking about functional programming and formal methods. In the past, I've contributed to mechanized Rocq proofs of some results in quantum computing. My academic background involves coursework in compilers, programming language theory, and type theory. Outside of these academic pursuits, I also enjoy building open source developer tools.

Moving forward, however, my career path is largely oriented toward industry, so to speak. I've nonetheless always tried to focus my attention on using functional programming languages. Previously, I interned at Pure Storage (now known as Everpure). More recently, I interned at Tesla, where I wrote Haskell; and at Jane Street, where I wrote OCaml. After graduation I will be joining Jane Street full-time as a software engineer.

My hobbies include philosophy, karaoke, poker, guitar, and crosswords. I also have a board game collection which rarely sees the light of day. This is a tragic but widespread and well-documented phenomenon—at least I can say none of my games are still in the original shrinkwrap. I'd rather be a board game player than a board game collector. I also care a lot about the particular tools I use. Though I used Neovim for a number of years, I have since switched to Emacs. I also use and love: Kitty, a terminal emulator; Kagi, a search engine; and Typst, a typesetting engine. Try them out! On another note, I have also taken it upon myself to read more fiction in the coming year. These days, I occasionally write code and even less frequently make videos.

I'd love to talk with you about anything! Reach me at michaellan AT ucla DOT edu.