Spécification mathématique de langages de programmation via les monades et leurs modules

Ambroise Lafont
Data61, CSIRO, Cogent team, Sydney
https://amblafont.github.io/

Date(s) : 29/04/2021   iCal
10 h 30 min - 11 h 30 min

La recherche dans le domaine des langages de programmation s’appuie traditionnellement sur une définition de syntaxe modulo renommage des variables liées, avec la sémantique opérationnelle associée. Nous nous intéressons à des outils mathématiques permettant de générer automatiquement la syntaxe et la sémantique à partir de données élémentaires. Nous portons une attention particulière à la notion de substitution, utilisant les notions catégoriques de monades et leurs modules. Les langages avec liaisons, telles que le lambda calcul pur, sont des monades sur la catégorie des ensembles. Nous proposons la notion plus complète de monades de transitions qui prend en compte également la sémantique opérationnelle. Nous donnons quelques exemples de spécifications de monades de transition, dans l’esprit de la Sémantique Initiale, selon lequel un objet est caractérisé par une propriété d’initialité dans une catégorie adéquate de modèles.

Mathematical specification of programming languages via monads and their modules

Research in the field of programming languages is traditionally based on a definition of modulo-renaming syntax of linked variables, with the associated operational semantics. We are interested in mathematical tools allowing to automatically generate syntax and semantics from elementary data. We pay particular attention to the notion of substitution, using the categorical notions of monads and their modules. Languages with bindings, such as pure lambda calculus, are monads on the category of sets. We propose the more complete notion of transition monads which also takes into account operational semantics. We give some examples of specifications of transition monads, in the spirit of Initial Semantics, according to which an object is characterized by a property of initiality in an adequate category of models.

https://hal.archives-ouvertes.fr/hal-02338144v3/

En visio-conférence ici :

  https://greenlight.lal.cloud.math.cnrs.fr/b/lio-hdc-jef

Catégories



Retour en haut