Thèse en preuves de programmes à VERIMAG Thesis on program proofs at VERIMAG lab

Conception d'une extension du calcul des constructions capable de générer des principes d'inductions pour des encodages de Church. Designing an extension to the Calculus of Constructions that can generate induction principles on Church encodings.

Utilisation de l'assistant de preuve Coq pour prouver la cohérence et la normalisation forte de cette extension. Using Coq to prove coherence and strong normalization properties for this extension.

Utilisation de Coq pour prouver la correction de certains algorithmes de la bibliothèque standard OCaml (par exemple, que son implémentation de MergeSort décrit bien un tri correct et stable). Using Coq to prove certain algorithms of the OCaml standard library (for example, that its implementation of MergeSort is correct and stable).

Administrateur de parc informatique à l'UFR IM²AG Systems administrator at the UFR IM²AG

Administration du parc informatique pédagogique et des serveurs de l'UFR IM²AG. Managing the lab computers and servers at the UFR IM²AG.

• Assistance technique de niveau 1 aux personnels de l'établissement, en lien avec la DSI de l'UGA Providing level 1 IT support to the UFR staff, escalating to central IT when necessary
• Déploiement d'images Linux/Windows avec CloneZilla en PXE Deploying Linux/Windows dual-boot images using CloneZilla over PXE
• Orchestration des mises à jour / installation de logiciels sous Linux via un serveur de paquets Debian locaux Orchestrating Linux updates / software installs via a local Debian package server
• Documentation des services et de l'infrastructure, dans un wiki partiellement accessible aux utilisateurs Maintaining infrastructure and service documentation in a semi-open wiki site
• Monitorat des postes grâce à TARSIS, un logiciel de monitorat d'infrastructure développé en interne Monitoring lab computers using TARSIS, and internally-developped program for infrastructure management