MGS 21 Abstracts
It is standard in the semantics of programming languages to use monads to model notions of computation that involve effects such as computation with input/output, manipulation of store, nondeterminism. Unlike a purely functional computation, an effectful computation cannot return a value on its own: it issues requests to the outside world and needs these responded to make progress. To run, it thus needs to be paired with an environment that is coeffectful, can service these requests. The two need to understand each other and work together. My message in this course is that environments and interaction are important characters in the act of computations. Notions of coeffectful environment are naturally modelled with comonads. Protocols of communication between computations and environments then admit mathematization by what we have christened interaction laws. I will give a brief general introduction to monads, comonads and their applications in semantics, but will then focus on interaction specifically. My material involves a fair amount of quite abstract constructions, but all come illustrated with concrete examples and almost all mean something for programming. I will need to assume basic knowledge of functional programming and some category theory (categories/functors/natural transformations, Cartesian closed categories). This course introduces the basics of category theory. I will cover categories, basic limits and colimits, duality, exponentials, functors, natural transformations and adjunctions. I hope to have time to briefly cover also monads and their algebras, and/or presheaves and the Yoneda Lemma. For each concept we will look at several examples. For these, I will assume some basic undergraduate mathematics and computer science, but hopefully the range of examples will be wide enough to be helpful for everyone. Our main reference is S. Awodey, Category theory, 2nd edition, Oxford Logic Guides 52. Type Theory is at the same time an alternative to set theory as a mathematical foundation and a programming language originally conceived by the Swedish philosopher and mathematician Per Martin-Löf. The course is an introduction to Type Theory, which covers the following topics:
I will use the Agda system for examples and exercises. Chapters from my forthcoming book (The Tao of Types) will be made available to the participants at my course web site. Proof theory is one of the "four pillars" of mathematical logic, and is of fundamental interest to mathematicians, computer scientists, philosophers and linguists alike. It serves as the foundation for many other endeavours in logic and has also been useful in realising the interplay between logic and other areas of mathematics, not least via the theory of computation. This course will introduce students to the world of proof theory from a computational perspective. The overall aim is to leave the student with an appreciation of how proof theory can be exploited to obtain interesting properties of logics, and how it relates to computation. Moreover this course should suffice to prepare a student for more advanced topics in logic and proof theory. Homotopy type theory is a formal system in which we can do mathematics. In this course, we will see how this works. In particular, we will learn how a mathematical statement is expressed, what the difference between synthetic (a.k.a. axiomatic) and analytic representation is, what univalence and higher inductive types are, and why truncation levels are important. No prior familiarity of homotopy type theory is assumed, but basic knowledge of both type theory and category theory will be helpful.
This course will provide an accessible, hands-on description of basic and advanced mechanisms for inductive and coinductive reasoning. It welcomes participants who use rigorous mathematical constructions in their day-to-day research and wish to widen their perspective on, and improve their arsenal of, practical induction and coinduction. All the concepts will be illustrated with examples and exercises formalized in the proof assistant Isabelle/HOL, taking advantage of the substantial extension of Isabelle/HOL's (co)induction infrastructure in recent years. People who already have some familiarity with Isabelle will make the most of the exercises. However, the presented concepts themselves are proof-assistant independent hence understandable without any knowledge of Isabelle. (Disclaimer: Though the participants will run the risk of becoming enthusiastic Isabelle users...) The topics covered range from basic ones such as
A detailed schedule of the course will soon be available from this website. References
This course is an introduction to call-by-push-value, a fine-grained calculus that subsumes both call-by-value and call-by-name lambda-calculus with computational effects (imperative features). After introducing the language, and the translations from call-by-value and call-by-name, we'll learn both operational and denotational semantics for a variety of effects: exceptions, I/O, state and control (continuations). This course is aimed at students with knowledge of typed lambda-calculus. I encourage students to read my course notes on typed lambda-calculus, at least up to Section 14, before the course. I will recap in the first lecture but rather quickly.
tbd |