Composition explores the intersections of art modalities, code, and mathematics.

Demos & Performances:

Isidore Mohr (isdra.bandcamp.com) - Girard's Paradox: Presentation and performance of my mathematical-proof-to-music translation system Soundproof. I livecode a proof of a contradiction, which Soundproof displays as music and visuals.

Claire Wang (ig @0xclaire) - Music, Proofs, and Dependent Types (talk + demo): Discussion and demo of two projects: Rocq N Roll, which turns tactics in the Rocq Prover into music, and a domain-specific language for counterpoint using the proof assistant Lean.

Micah Fitch (https://wondering.xyz) - Polyphonotypes: A theoretical framework and tools for mapping and understanding relationships between pitch-class sets. Think *circle of fifths meets graph theory* and then they discover that they're both interested in learning more about monoidal categories (surprise!).

Brian Abelson (brian.abelson.live, ig @abelsonlive) - saysynth: Discussion and demo of a synthesizer I built on top of Mac's text-to-speech framework. You can read the documentation on the software here: https://docs.saysynth.org/saysynth.html. Recordings of the demos are here: https://abelsonlive.bandcamp.com/album/saysynth

Conversation: "Compiling" to interactive dynamic sequencers? (led by Micah Fitch)

Let's cross pollinate musical, mathematical and computer scientific perspectives.

What's the difference between a "computer program" and an "interactive, realtime dynamic sequencer?" Is there one? Why should there be? What could it look like to design a compiler meant for interpreting declarative specifications of dynamic, realtime interactive sequencers for interactive multimedia purposes and more?

How might [insert theoretical perspective] help us frame this?