I present a translation of Girard’s Paradox into music using Soundproof, an in-progress system for translating proof terms of dependently typed lambda calculus into electronic music according to their tree structure. I explore methods of representing tree structures sonically, and points of choice in the translation and presentation of the result.