
Mathematically Structured Programming group @UniStrathclyde We are interested in type theory, category theory, and how to stop seeing them as different things.
- Tweets84
- Following17
- Followers815
- Likes42

ALT Protocol Verification Lecturer: Andrés Goens Abstract Protocols are central to the functioning of many crucial systems. From the consistency of your device's memory, to exchanging information over the internet, protocols ensure these extremely concurrent systems function correctly. In this course we will consider some basic principles required to verify such protocols. We will learn about labeled transition systems and use temporal logic to specify properties of them. In particular, we will focus on safetey and fairness conditions in protocols.

ALT Effects and Handlers Lecturer: Sam Lindley Abstract Effect handlers allow programmers to define, customise, and compose a range of crucial programming features ranging from exceptions to lightweight threads to probability, inside the programming language. In this course I will give a high-level introduction to the theory of algebraic effects and effect handlers, effect type systems for effect handlers, and effect handler oriented programming.

ALT Applied Category Theory Lecturer: Jules Hedges Abstract This course will be about symmetric monoidal categories and what they have to tell us about computation and systems. I plan the topics of my 4 lectures to be: string diagrams as 2-dimensional syntax, how they unify computation graphs and flowcharts traced, compact closed and hypergraph categories, non-well-founded recursion, backtracking and quantum processes decorated and structured cospans, the standard sledgehammer for building domain-specific categories of open systems bidirectional processes: lenses, optics, containers, differentiable programming, categorical cybernetics






