Marc Coiffier Administrateur système Systems administrator
📧 marc@coiffier.net
☎ 06 59 83 75 00
🎂 28 Juin 1991June 28th, 1991
🏠
15, allée des Vosges
38130 Échirolles

Savoir-êtreSkills

Empathie Empathy Curiosité Curiosity Adaptabilité Adaptability Travail en équipe Teamwork Esprit d'initiative Initiative Persévérance Tenacity Politesse Politeness

Savoir-faireCompetences

Administration système (Debian, ArchLinux, NixOS) Systems administration (Debian, ArchLinux, NixOS) Automatisation / Déploiement (Docker, Nix, CI/CD, ...) Automation / Deployment (Docker, Nix, CI/CD, ...) Anglais courant Fluent english Programmation fonctionnelle (Haskell, OCaml) Functional programming (Haskell, OCaml) Développement collaboratif (Git, GitHub, SourceHut, ...) Collaborative development (Git, GitHub, SourceHut, ...) Programmation de bas niveau (C, C++, Rust) Low-level programming (C, C++, Rust) Méthodes formelles (Coq) Formal methods (Coq) Développement Web (PHP, JS, React, CSS, Tailwind, ...) Web development (PHP, JS, React, CSS, Tailwind, ...)

Expériences professionnelles Experience

2016-2020

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

2012-2016

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

Projets personnels Personal projects

Curly : un compilateur pour un langage fonctionnel simple Curly : a compiler for a simple functional language

Lien vers le projetLink to the project

Un compilateur développé en Haskell, capable de builds reproduisibles et multi-plateformes. A simple compiler, written in Haskell, that enforces reproducible cross-platform builds.

  • Un système de type capable d'inférer des types récursifs (comme λx.xx) A type-system that can infer recursive types (as with the term λx.xx)
  • Des classes de types de premier ordre First-class typeclasses
  • Une édition des liens en une seule passe, pour une génération de code assembleur en just-in-time ou en éxécutable statique Single-pass linking, for just-in-time and static executable assembly code generation
  • Des modules content-addressed pour rendre la compilation reproduisible par défaut Content-addressed modules to provide reproducible builds by default
  • Un format de documentation intégré au compilateur, et une documentation de second ordre (fini les commentaires de documentation) Built-in documentation format, and second-order documentation (no more doc comments)
  • Du Code-signing automatique lors de la distribution de modules Automatic code-signing when distributing modules

Omega : un micro-kernel Omega : a micro-kernel

Lien vers le projetLink to the project

Un projet d'apprentissage, qui m'a permis d'en apprendre beaucoup sur la façon dont les systèmes d'exploitation fonctionnent, dans les moindres détails. A toy projet that taught me a lot about the way operating systems work internally.

  • Multi-processus avec protection de la mémoire Multi-process with memory protection
  • Multi-thread avec synchronisation inter-processus Multi-thread with inter-process synchronisation
  • Doté d'un langage de script et d'une CLI Complete with basic CLI and a scripting language
  • Drivers clavier, et VGA rudimentaire Rudimentary keyboard, and VGA, drivers
  • Très rapide à démarrer ! Blazing fast to boot !

Viz : un visualiseur de réseaux d'interaction Viz : an interaction network visualizer

Lien vers le projetLink to the project

Dans le but de développer un algorithme beta-optimal d'évaluation du calcul des constructions, qui se repose sur l'utilisation de réseaux d'interaction. In order to design a beta-optimal evaluator for the Calculus of Construction, that uses interaction nets.

  • Création et suppression de noeuds et d'arêtes, dans un canvas SVG Create and delete nodes and edges in an SVG canvas
  • Application de règles de réduction pour visualiser les étapes intermédiaires de réductions complexes Apply reduction rules to see how the graph evolves
  • Repositionnement automatique des noeuds du graphe pour minimiser la "tension interne" et rendre la visualisation plus lisible (utilise la descente de gradient) Automatically smooth reposition nodes to minimize "internal tension" and make visualization more legible (uses gradient descent)

DiplômesEducation

2016

Ingénieur Réseaux et Télécommunications Network Engineer

Validation des acquis d'expérience (VAE) après 4 années d'administration système à l'UFR IM²AG Knowledge acquired by experience after 4 years' working as a systems administrator at the UFR IM²AG.

2011

Maths and Computer Science LicentiateLicence Mathématiques et Informatique

À l'Université Joseph Fourier de Grenoble At the Université Joseph Fourier in Grenoble

2008

Baccalauréat GénéralBachelor's Degree

Au lycée Champollion de Grenoble At the Champollion High School in Grenoble

Centres d'intérêtInterests

Musique : piano, violon et guitareMusic : piano, violin and guitar Danse : Lindy Hop avec Grenoble Swing et danses folk à l'Escapade Folk Dance : Lindy Hop with Grenoble Swing and traditional dances with the Folk Escapade Jeux de société à la Maison des Jeux de Grenoble Board games with the Grenoble Games' Den