“Logical Soundness” aims to express a mathematical proof in a way so that the basic structure of the proof is audible. Elements of the proof are represented as musical motifs, and other aspects may modify the music or sound. Recursive aspects of the proof are also represented, for example by doubling the speed.

I have chosen a soundness proof to express in sound, in particular lemma 4.3 of this paper. This proof has been formalized in Agda. Also using Agda, my own program uses reflection to get the intermediate representation of the proof, and converts this into music using a mapping from names to motifs, maintaining the basic structure. It uses my library MusicTools to handle most of the work and generate a MIDI file as output.