2026-06-04
Carnegie Mellon University
Pittsburgh, PA

This artifact is from a one-on-one meeting I had with Dr. Fabian Muehlboeck when he visited as a guest speaker at the undergraduate research experience program I was attending at Carnegie Mellon University.

Dr. Muehlboeck typed out this artifact from memory on my laptop after I asked him to elaborate more on the distinction between type system soundness and decidability. He noted that the Java type system is also unsound, but that the point of this artifact was to show that it is undecidable.

I expressed my gratitude for the meeting, sharing of knowledge, and the very interesting example program.

Dr. Muehlboeck's research is currently focused on improving the usability and performance of gradual type systems for practical use, and I found his lecture both informative and interesting.

In particular, I was made aware of the extreme performance overhead that can come from introducing gradual typing, which could make certain applications of it unusable. Dr. Muehlboeck has published work on ways to reduce gradual type system overhead by orders of magnitude, which I found to be of particular note.