Marc Coiffier Développeur et ingénieur système Developper and systems engineer

📧 marc@coiffier.net
06 59 83 75 00
🎂 28 Juin 1991June 28th, 1991
🏠
15, allée des Vosges
38130 Échirolles

💬 Français / English
🖨 Version imprimable PDF version
🌐 CV en ligne Online résumé

Savoir-êtreSkills

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

Savoir-faireCompetences

Programmation fonctionnelle (Haskell, OCaml) Functional programming (Haskell, OCaml) Anglais courant Fluent english Administration système (Debian, Linux, bash, ...) Systems administration (Debian, Linux, bash, ...) Intégration continue / builds reproduisibles (Docker, Nix, CI/CD pipelines, ...) Continuous integration / reproducible builds (Docker, Nix, CI/CD pipelines, ...) Méthodes formelles (Coq) Formal methods (Coq) Programmation de bas niveau (C, C++, Rust) Low-level programming (C, C++, Rust) Développement collaboratif (Git, GitHub, SourceHut, ...) Collaborative development (Git, GitHub, SourceHut, ...) 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 de l'UFR IM²AG. Managing the lab computers of the UFR IM²AG.

Installation, déploiement et maintenance de près de 400 machines à disposition pour l'enseignement de l'informatique, ainsi que d'une dizaine de serveurs, dont un cloud Proxmox, un dépôt Debian local, plusieurs serveurs d'application Web, un serveur de monitorat, un annuaire LDAP, un serveur PXE, et d'autres encore. Installing, deploying and maintaining close to 400 computers made available to university students and teachers, as well as a over a dozen servers, including a Proxmox private cloud, a local Debian package repository, multiple Web application servers, a monitoring server, an LDAP directory, a PXE server, and more.

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éduction 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