Dr. Richard Garner & Professor Dominic Verity, Macquarie University
Theoretical computer science enables us to reason in a mathematically rigorous way about computation: for example, proving that a given program is error-free. Much of this reasoning makes use of category theory, an abstract meta-language for mathematical discourse. This course will give an introduction to category theory with an emphasis on various kinds of monoidal category (category with formal tensor product); and apply monoidal category theory to the study of topics from computer science, for example concurrent computing, games for semantics, and Girard’s linear logic.
The course will start with an introduction to basic notions of category theory: categories, functors, natural transformations and the concept of free construction. The further theory covered by the course will deal with notions of monoidal category, including notions such as:
- braided and symmetric monoidal categories;
- internal homs and duals (monoidal closed categories, *-autonomous categories, compact closed categories, cartesian closed categories;
- traced monoidal categories.
We will use these theoretical notions to study notions from computer science in a mathematically rigorous way, dealing with, for example:
- concurrent systems (categories of Petri nets/event structures);
- linear logic and *-autonomous categories;
- monoidal categories of games (including the Joyal approach to Conway games);
- Girard’s geometry of interaction.
The two strands, the theory and the applications, will be interleaved over the course’s duration.
28 hours, made up of 20 hours of lectures and 8 hours of tutorials.
Please see the Timetable for scheduled class times during the AMSI Summer School 2017.
Please note: Category Theory and Computer Science is held concurrently with Mathematical Biology and students cannot attend both courses in 2017.
No strict prerequisites, but a familiarity with basic algebraic notions (groups, vector spaces) may be helpful. We will not assume any prior knowledge of computer science.
- Two assignments: 20% each
- Final examination: 60%
Dr. Richard Garner, Macquarie University
Richard’s journey into the mathematical realm began in earnest with undergraduate and doctoral degrees from the University of Cambridge; after receiving his Ph.D. in 2006, he held postdoctoral positions at Uppsala University and at Cambridge before moving to Australia in 2010 to join Macquarie University’s Centre of Australian Category Theory. His research interests lie in the area of category theory and its applications to logic, geometry, topology and computer science.
Professor Dominic Verity, Macquarie University
Dom started his computational career in the very early 1980s as a software developer for the legendary British personal computing pioneer Acorn Computers, the company which created the BBC Microcomputer and ultimately invented the ubiquitous ARM microprocessor. He went on from there to work for the BBC World Service, where he was involved in designing and developing microcomputer technologies for application in radio production departments.
He studied as both an undergraduate and postgraduate at the University of Cambridge (UK) and emerged from that institution in 1992 with a PhD in Mathematics. From 1994 to 2000 he worked in the investment banking industry, as a mathematical consultant in derivative securities valuation and hedging, as a quantitative analyst in equity derivatives for Deutsche Bank Australia and as the Head of Equity Derivatives Trading for HSBC Australia.
He returned to academe in late 2000, and since then he has worked as a mathematician and computer scientist at Macquarie University. His research interests lie in the mathematical fields of Homotopy Theory, sometimes known as “rubber sheet geometry”, and Category Theory, a kind of “theory of everything” for pure mathematics. In recent years, he has held visiting Professorship positions at Harvard University, Johns Hopkins University, and the University of Cambridge.
Dom is a passionate and engaging teacher of Computer Science and in 2011 he gained national recognition for his work as an educator with the award of an Australian Learning and Teaching Council Citation for Outstanding Contribution to Student Learning “for a decade of inspirational and innovative educational leadership in the field of information technology”.
Over the past decade, Dom has been highly active in academic leadership roles at the Department, Faculty and University levels. Most recently he has led Macquarie’s academic governance as Chair of its Academic Senate, which is the “principal academic body in the University”.