Off the Beaten Track 3: Proofs as Stories
Off the Beaten Track was Languages for Computational Creativity: Generative Art and Interactive Worlds, by Chris Martens. Her talk included the most inventive application of Propositions of Types that I ever heard: Proofs as Stories. Later, she provided a citation to a longer work, Linear Logic for Non-Linear Storytelling, by some of her collaborators, which uses proofs in linear logic to describe alternative storylines for Madame Bovary. Thanks, Chris!