Sémantiques mécanisées : quand la machine raisonne sur ses langages

Documents et médias

Télécharger le programme

pdf (276.99 Ko)

Programme

Cours

09:30 - 11:00

L'éternité, c'est long : divergence, théorie des domaines, approches coinductives

Xavier Leroy

30 jan 2020

Sémantiques mécanisées : quand la machine raisonne sur ses langages

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Interpréteurs abstraits mécanisés

David Pichardie

30 jan 2020

Sémantiques mécanisées : quand la machine raisonne sur ses langages

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Des fonctions et des types : la sémantique d'un langage fonctionnel

Xavier Leroy

06 fév 2020

Sémantiques mécanisées : quand la machine raisonne sur ses langages

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Understanding and Evolving the Rust Programming Language

Derek Dreyer

06 fév 2020

Sémantiques mécanisées : quand la machine raisonne sur ses langages

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

What's in a Name? Représenter les variables et leurs liaisons

Xavier Leroy

13 fév 2020

Sémantiques mécanisées : quand la machine raisonne sur ses langages

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Coq en Coq ? Mécaniser la logique d'un assistant à la démonstration

Xavier Leroy

13 fév 2020

Sémantiques mécanisées : quand la machine raisonne sur ses langages

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

13 fév 2020

10:45 - 12:15

Voir aussi

Cours en relation avec le séminaire : Sémantiques mécanisées : quand la machine raisonne sur ses langages

Xavier Leroy, chaire Sciences du logiciel

Sémantiques mécanisées : quand la machine raisonne sur ses langages

Documents et médias

Programme

Des expressions et des commandes : la sémantique d'un langage impératif

Traduttore, traditore : vérification formelle d'un compilateur

Lambda, the Ultimate Teaching Assistant (Agda Version)

Compiler mieux : optimisations, analyses statiques, et leur vérification

L'arithmétique des ordinateurs et sa formalisation

Des logiques pour raisonner sur les programmes

Sémantique formelle de JavaScript : les enjeux du passage à l'échelle

Un art abstrait : l'analyse statique par interprétation abstraite

Logique de séparation en Coq : théorie et pratique

L'éternité, c'est long : divergence, théorie des domaines, approches coinductives

Interpréteurs abstraits mécanisés

Des fonctions et des types : la sémantique d'un langage fonctionnel

Understanding and Evolving the Rust Programming Language

What's in a Name? Représenter les variables et leurs liaisons

Coq en Coq ? Mécaniser la logique d'un assistant à la démonstration

Voir aussi