Administrateur système et réseaux à l'IPAG Systems administrator at the IPAG

Administration du parc informatique de l'IPAG, un institut de planétologie regroupant plus de 150 utilisateurs, requérant une variété d'environnements et outils informatiques Managing the computer infrastructure at the Insitute of Planetology and Astrophysics in Grenoble, totalling more than 150 users requiring a variety of tools and environments

Développement d'un logiciel de "self-service" sous Linux, afin de proposer aux utilisateurs du laboratoire un catalogue de logiciels adaptés à leur activités, et installables en un clic. Developed an "app store" that runs on Linux, to present our users with a curated list of research-specific applications, that they can install in one click.

Conception, développement et déploiement d'une application Web de monitorat de parc informatique pour faciliter le maintien de la PSSI (politique de sécurité des services informatiques) Designed, developed and deployed a Web application to help in monitoring the institute's computers, and in maintaining compliance with our IT Security Policy

Participation au projet de développement de code communautaire Idefix, en collaboration avec Geoffroy Lesur, et travail sur l'intégration continue du projet dans des environnements HPC divers (cluster Jean-Zay à l'IDRIS, Adastra à GENCI et Bigfoot à GRICAD) Participating in the community project Idefix, and collaborating with Geoffroy Lesur to work on the continuous integration of the project into various HPC environments (Jean-Zay at IDRIS, Adastra at CINES, and Bigfoot at GRICAD)

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).

Développement d'un "wiki" de preuves, site statique écrit en Markdown littéraire permettant d'explorer et de vérifier des fragments de preuves directement sur le navigateur Developing a "proof wiki", a static site generated through literate programming, that allows exploration and verification of proofs in the browser.

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