Pour la réunion des 17 et 18 octobre 2024, suivre ce lien.
Lieu: Salle Emmy Noether, Centre Inria de Paris, 48 rue Barrault, 75013 Paris
La logique de la théorie des types est naturellement restrictive vis-à-vis de l'égalité entre les fonctions. Pour réécrire dans une intégrale ou une somme itérée, la façon idiomatique de faire des preuves est de faire explicitement appel à un lemme (ou un axiome) d'extensionalité. En revanche, l'usage en mathématiques est d'utiliser l'extensionalité de façon implicite. Dans cet exposé, nous décrivons des expériences pour réduire la distance entre les différentes habitudes.
Overloading consists of using a same symbol to refer to several functions, or a same same to refer to several constants. Overloading is ubiquitous in mathematics. It also appears in numerous programming languages that resolve overloading statically, as opposed to languages that rely on dynamic dispatch during program execution. Thus, a key question is how to determine, for every occurrence of an overloaded symbol, which function it refers to. Static resolution of overloading is intrinsically intertwined with typechecking. Indeed, overloading resolution depends on types, but the types of the overloaded symbols depend on how they are resolved. This work presents the first typechecking algorithm for static resolution of overloading that: (1) guides resolution not only by function arguments but also by expected result type, and (2) supports polymorphic types. Moreover, our algorithm supports type inference like traditional ML typecheckers—we only exclude inference of polymorphism. We illustrate the practicality of our algorithm for typechecking conventional mathematical formulae, as well as for typechecking ML code with overloading of literals, functions, constructors, and record field names.
Les preuves mathématiques sont souvent représentées de manière très graphique, et d'une manière assez différente de celle de Rocq. Le but ici est de réfléchir à quoi pourrait ressembler l'interface Rocq avec une composante visuelle, en restraignant le sujet au plus simple des objects graphiques : un tableau de variation. Je vais vous présenter les expériences que nous avons fait à Grenoble, ainsi que l'interface que nous proposons.
Liber Abaci mid-term review Hosted by Yves Bertot https://inria.webex.com/inria-en/j.php?MTID=md55ccb4354de937d1ada975486d63055 Wednesday, March 12, 2025 9:00 AM | 9 hours | (UTC+01:00) Brussels, Copenhagen, Madrid, Paris Meeting number: 2744 945 4067 Password: zkMUayZ4H43 Join by video system Dial 27449454067@inria.webex.com You can also dial 62.109.219.4 and enter your meeting number. Join by phone +33-1-8514-8835 France Toll 2 Access code: 274 494 54067