(TBA)

The forthcoming edition of POPL will feature a rather elegant piece [https://www.cl.cam.ac.uk/~ds709/agda-soas/formal-metatheory-of-soas.pdf] by M. Fiore and D. Szamozvancev on the implementation of intrinsic syntaxes in type theory, using the usual categorical tools (initial algebra semantics, presheafs, etc.) as an effective blueprint for the construction.

I propose (rather: Adrien has volunteered me) to show up with an Agda buffer and offer a live tour and commentary of the code.

We extend classic union and intersection type systems with a type-case construction and show that the combination of the union elimination rule of the former and the typing rules for type-cases of our extension encompasses “occurrence typing”. The latter is a typing technique that takes into account the result of type tests to assign different types to a same expression when it occurs in different branchings of the test.

To apply this system in practice, we define a canonical form for the expressions of our extension, called MSC-form. We show that an expression of the extension is typable if and only if its MSC-form is, and reduce the problem of typing the latter to the one of reconstructing annotations for that term. We provide a sound algorithm that performs this reconstruction and a proof-of-concept implementation.

Cython+ est un projet expérimental d'extension du compilateur Cython sur lequel je travaille depuis un an et demi.

Cython permet de joindre Python et C/C++ au sein d'un même langage. L'intérêt majeur de Cython est qu'il rend facile l'utilisation de code C/C++ comme back-end de code Python. On peut ainsi contourner le GIL de Python (le verrou global qui ne permet qu'à un seul thread à la fois d'exécuter du bytecode Python dans l'interpréteur CPython).

Avec Cython+, nous étendons les possibles de Cython sur trois aspects: 1. Tout d'abord, nous introduisons un système d'objets utilisables sans le GIL en exécution multi-thread sur plusieurs coeurs. La gestion de la mémoire est automatique comme en Python grâce à un comptage de références atomique. De plus une couche de compatibilité transparente en fait de vrais objets Python manipulables en tant que tels directement depuis l'interpréteur Python. 2. De plus, nous ajoutons à cela un modèle d'exécution asynchrone à base d'acteurs et une implémentation d'un scheduler inspiré par celui de Go. 3. Enfin, nous sommes en train d'explorer un système de types pour la thread safety inspiré par ceux de Pony et Rust.

Reactive systems, which are omnipresent from airplanes to videogames, execute in continuous interaction with their environment. Functional reactive programming (FRP) aims to describe these systems as mathematical functions between the infinite streams of their inputs and outputs.

Several lines of research have enriched this approach with strong type systems: works based on Nakano's guarded recursion use type-theoretical modalities to guarantee productivity. While this approach has its benefits, many of such domain specific functional languages fail to have a runtime suitable for resource-scarce environments. Such environments usually use the synchronous programming paradigm, which uses more specialized methods, but gives strong guarantees on the efficiency of the program.

In this presentation, we aim to present a recent synthesis between the two approaches by describing how a FRP language can be given a semantics in the synchronous style. We will then investigate the potentially deeper connections between synchronous programming and FRP.

In this introductory session of the reading group, we will read, discuss and dissect the following two papers

1. Learning to Prove Theorems via Interacting with Proof Assistants
2. TacTok: semantics-aware proof synthesis

In the context of the development of the Coq proof assistant, I have created and maintained a multi-function bot to assist developers in automating some basic and repetitive tasks. In this talk, I will present a recent pull request that was submitted to the bot repository and this will be an opportunity to present the way the bot is architectured, and how it uses a modern, typed, GitHub API and suitable OCaml libraries to implement its features, and how that makes it easy to extend.