Applied Category Theory  The Emerging Science of Compositionality
What do programming, quantum physics, chemistry, neuroscience, systems biology, natural language parsing, causality, network theory, game theory, dynamical systems and database theory have in common?
As functional programmers, we know how useful category theory can be for our work  or perhaps how abstruse and distant it can seem. What is less well known is that applying category theory to the real world is an exciting field of study that has really taken off in just the last few years. It turns out that we share something big with other fields and industries  we want to make big things out of little things without everything going to hell! The key is compositionality, the central idea of category theory.
This talk will introduce the emerging field of applied category theory, with the aims of:
 Giving attendees a broad overview of cuttingedge applications of category theory
 Building an understanding of a small number of the most important core concepts
 Getting attendees excited, inspired to learn more, and equipped to apply some basic concepts to their work
Outline/Structure of the Talk
The basic approach is to spend the audience's attention budget wisely on a small number of carefully chosen theoretical concepts, but otherwise leave the audience with a clear motivating picture regardless. Full advantage will be taken of the convenient and intuitive graphical representations that category theory enables, like string diagrams.
Talk structure:
 Motivation  what's applied category theory about. Introducing the key concept of compositionality, and string diagrams.
 Highlevel overview of the emerging field of applied category theory; a casebycase look at some exciting applications, touching briefly on quantum physics, DNA sequencing, US military search & rescue systems, and database migrations. This section will avoid technical details of the different fields, and focus on giving a sense of how category theory relates to what they do.
 Teaching selected theoretical concepts: monoidal categories which allow string diagrams, and cospans, operads which allow wiring diagrams. I will probably omit advanced aspects such as weakness/strictness, associators, unitors and the pentagon laws, since they are implicit in string diagrams anyway, and I need the "attention budget" for other stuff. I will also set up wiring diagrams, which seem to be of obvious and immediate utility to programmers. I will use software design as a familiar motivation for both.
 Conclusion  why applied category is so exciting. Where to go to learn more, who to follow, what to read.
Learning Outcome
After attending, the audience should:
 Understand the motivation for the field of applied category theory
 Have a basic understanding of how it applies to different industries & fields
 Have a basic theoretical understanding of monoidal categories
 Be able to use string diagrams and wiring diagrams in their own work designing software
 Ideally, be as excited as me
Target Audience
Functional programmers
Prerequisites for Attendees
A rudimentary understanding of the basic concepts of category theory will be helpful (but not essential), as I will spend very little time setting up categories and functors. I will assume that the audience are programmers and are familiar with the nature of software development and design.
Links
I have given a number of talks at different conferences and events, including a talk about Category Theory at Lambda Jam 2015. https://www.youtube.com/playlist?list=PLns2Qlp9mGyFAniFLczjJle5B8mxD35e
I'll draw on various ACT resources, including:
 "What is Applied Category Theory?" by Tae Danae Bradley https://arxiv.org/abs/1809.05923
 "Seven sketches in compositionality: an invitation to applied category theory" by Brendan Fong & David Spivak https://arxiv.org/abs/1803.05316
 "Applied Category Theory Course" by John Carlos Baez https://johncarlosbaez.wordpress.com/2018/03/26/sevensketchesincompositionality/
 "The operad of wiring diagrams: formalizing a graphical language for databases, recursion and plugandplay circuits" by David Spivak https://arxiv.org/abs/1305.0297
 "Decorated Cospans" by Brendan Fong https://arxiv.org/abs/1502.00872
 "Complex Adaptive System Design" (parts 18) by John Carlos Baez https://johncarlosbaez.wordpress.com/2016/10/02/complexadaptivesystemdesignpart1/
schedule Submitted 3 months ago
People who liked this proposal, also liked:

keyboard_arrow_down
Philip Wadler  (Programming Languages) in Agda = Programming (Languages in Agda)
Philip WadlerProfessor of Theoretical Computer ScienceUniversity of Edinburghschedule 2 months ago
60 Mins
Keynote
Beginner
The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that propositions correspond to types, proofs to programs, and simplification of proofs to evaluation of programs. The proof of a conjunction is a pair, the proof of a disjunction is a case expression, and the proof of an implication is a lambda expression. Proof by induction is just programming by recursion.
Dependentlytyped programming languages, such as Agda, exploit this pun. To prove properties of programming languages in Agda, all we need do is program a description of those languages Agda. Finding an abstruse mathematical proof becomes as simple and as fun as hacking a program. This talk introduces *Programming Language Foundations in Agda*, a new textbook that is also an executable Agda scriptand also explains the role Agda is playing in IOHK's new cryptocurrency.

keyboard_arrow_down
Bartosz Milewski  A Taste of Type Theory
60 Mins
Keynote
Beginner
We use types in programming, often without realizing how deeply rooted they are in the foundations of mathematics. There is a constant flow of ideas from type theory to programming (and back). We are familiar with algebraic data types; inductive types, like lists or trees; we've heard of dependent types and, in the future, we might encounter identity types and possibly get familiar with elements of homotopy type theory. I can't possibly talk about all of this, but I'll try to give you a little taste.

keyboard_arrow_down
Andy Kitchen  Metaquines
30 Mins
Talk
Beginner
A quine is a program that outputs its own source code, but can you create a 2 quine, a pair of programs that output each other with an A>B>A>B cycle? What about between different languages? Can you gzip your own source code? Is there a structured way to do this with theory? All these questions will be somewhat answered, in ways that will make your head hurt... mathamagical demos and over 9000 layers of metaness await!

keyboard_arrow_down
Attila EgriNagy  Approaching the Yoneda Lemma
Attila EgriNagyAssociate Professor of MathematicsAkita International Universityschedule 1 month ago
30 Mins
Talk
Intermediate
The Yoneda lemma is not the first thing to learn in category theory, but sooner or later it appears in studying the field. Unfortunately, there is quite a gap between the intuitive idea, "tell me your friends, and I will know who you are" , and its precise formulation. This talk aims to bridge this gap by introducing algebraic results in the middle, namely Cayley's theorem for groups and its generalization to semigroups. These are elementary enough, but at the same time they exhibit the conceptual step of representability, and the idea of studying all different things in a familiar form.

keyboard_arrow_down
Attila EgriNagy  The rules of the game
Attila EgriNagyAssociate Professor of MathematicsAkita International Universityschedule 1 month ago
30 Mins
Talk
Beginner
In the postAlphaGo era there is no need for introducing the game of Go. It is one of the most complex games with very simple rules. But wait a minute, how simple are they exactly? ... different solutions for a problem with clashing requirements, leading to endless debates; edge cases where specifications offer no help; complexity hopeless to tame... Are we still talking about the game, or about software development?!? Well, both. This may come as a surprise, but there is no agreement on the rules of Go. The different rule sets are compatible most of the time, but when they disagree, they do it in a big way in deciding who is the winner. Can we fix the rules then? There are researchers working on the problem, but the perfect rule set is as elusive as the perfect software application.
This talk is a cautionary tale about the power and limits of formalization, and how humans relate to formal specifications. We will discuss the different rule sets, analyze their differences. The `simple' case of Go will serve as an analogue for software specifications and foundations of Mathematics.