A translation of the reduction behavior of Girard’s paradox into music using Soundproof, a tool for making music from terms of the dependently typed lambda calculus. I present the extension of the tool from single-term to reduction-based translation, and discuss points of choice in the small-step interpreter and its musical output.
Ahmet Yigit Erdem Institute of Science Tokyo, Middle East Technical University, Ari Prakash Northeastern University, Carlo Angiuli Indiana University, Rose Bohrer National Institute of Advanced Industrial Science and Technology (AIST), Japan, James McCann Carnegie Mellon University, Chris Martens Northeastern University, Youyou Cong Institute of Science Tokyo