Free Foil в спокойном темпе

Планируется 5 выступлений на три недели (начиная со среды 4 сентября)
Предварительно тематический план следующий: (1) Introduction to Capture-Avoiding Substitution, Rewriting, and Higher-Order Unification. In this talk, I will explain the problems that arise when working with bound names (e.g. local variables) and their practical implications for the implementation of modern compilers, proof assistants, and theorem provers. The applications are covered superficially, to provide motivation for the next talks. (2, optional) De Bruijn Notation and Locally Nameless Representations. This talk focuses on several variations of "locally nameless" representations, including de Bruijn indices, the locally nameless representation of Arthur Chargueraud, de Bruijn notation as nested data types a la Bird and Paterson, generalized generalized de Bruijn notation a la Kmett, and co-de Bruijn indices of McBride. (3, optional) Higher-Order Abstract Syntax. This talk focuses on a family of techniques that "cheat" the problem of name binders by reusing the binders of the host language (which can be any language with support for higher-order functions). In particular, we will look at both classical HOAS and parametric HOAS (PHOAS). (4) The Barendregt convention, the Rapier, and the Foil. In this talk, we will discuss three implementations of the Barendregt convention: a naive implementation, an efficient algorithm used in GHC and Agda, and a novel safe version of the latter, used in the implementation of the Dex programming language. (5) Free Scoped Monads and Free Foil. We now split syntax into two its signature (specification of syntactic constructions) and the recursive structure with variables and binders (which can be handled generically). Such separation enables a kind of generic programming: it is now possible to implement certain algorithms once for (almost) any language with binders. Apart from relatively straightforward capture-avoiding substitution, we also mention the ability to implement alpha-equivalence, conversion functions, and non-trivial higher-order unification algorithms (at least in principle).
К сожалению, организаторы семинара вынуждены отложить серию докладов Н.Д. Кудасова (которая изначально планировалась с 4 по 20 сентября). О времени, когда состоится эта серия докладов Н.Д. Кудасова, будет объявлено дополнительно.