{"id":9,"date":"2018-01-26T09:27:47","date_gmt":"2018-01-26T09:27:47","guid":{"rendered":"http:\/\/vm-web-qualif.pun.ens-lyon.fr\/lip-cash\/?page_id=9"},"modified":"2026-09-28T15:13:52","modified_gmt":"2026-09-28T13:13:52","slug":"contact","status":"publish","type":"page","link":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/?page_id=9","title":{"rendered":"Members"},"content":{"rendered":"\n<h1 class=\"wp-block-heading\">Permanent Members<\/h1>\n\n\n\n<h2 class=\"wp-block-heading\">Christophe Alias<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">Researcher at <a href=\"https:\/\/www.inria.fr\/\">Inria<\/a>.<br>Keywords: compilation, high-level synthesis, polyhedral model.<br>Home page: <a href=\"http:\/\/perso.ens-lyon.fr\/christophe.alias\/\">http:\/\/perso.ens-lyon.fr\/christophe.alias\/<\/a>, <a href=\"https:\/\/hal.archives-ouvertes.fr\/search\/index\/q\/%2A\/authIdHal_s\/christophe-alias\/\">List of publications<\/a><\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Aur\u00e8le Barri\u00e8re<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">Researcher at <a href=\"https:\/\/www.cnrs.fr\/\">CNRS<\/a>.<br>Keywords: formal verification, compilation, regular expressions, Rocq.<br>Home page:&nbsp;<a href=\"https:\/\/aurele-barriere.github.io\">https:\/\/aurele-barriere.github.io<\/a>, <a href=\"https:\/\/cv.hal.science\/aurele-barriere\">List of publications<\/a><\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Cyril Cohen<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">Researcher at <a href=\"https:\/\/www.inria.fr\/\">Inria<\/a>.<br>Keywords: proof assistants, type theory, Rocq, formalization of mathematics, mathcomp.<br>Home page: <a href=\"http:\/\/cyrilcohen.fr\">http:\/\/cyrilcohen.fr<\/a>, <a href=\"https:\/\/cv.hal.science\/cyril-cohen\">List of publications<\/a><\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Ludovic Henrio (team co-leader)<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">Researcher at <a href=\"https:\/\/www.cnrs.fr\/\">CNRS<\/a>.<br>Keywords: programming languages, actors, semantics, concurrency and distribution, objects, components, futures.<br>Home page: <a href=\"https:\/\/lhenrio.github.io\/\">https:\/\/lhenrio.github.io\/<\/a>, <a href=\"https:\/\/cv.archives-ouvertes.fr\/ludovic-henrio\/\">List of publications<\/a><\/p>\n\n\n\n<h2 class=\"wp-block-heading\">S\u00e9bastien Michelland<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">Assistant professor at <a href=\"https:\/\/ens-lyon.fr\">ENS de Lyon<\/a>.<br>Keywords: security, hardware, compilation.<br>Home page: TBA, <a href=\"https:\/\/hal.science\/search\/index\/q\/*\/authFullName_s\/S%C3%A9bastien+Michelland\">List of publications,&nbsp;<\/a><\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Matthieu Moy (team co-leader)<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">Assistant professor at <a href=\"https:\/\/www.univ-lyon1.fr\/\">UCBL (Lyon 1)<\/a>.<br>Keywords: hardware simulation, compilation, many-core, dataflow languages, formal verification, digital frugality.<br>Home page: <a href=\"https:\/\/matthieu-moy.fr\">https:\/\/matthieu-moy.fr<\/a>, <a href=\"https:\/\/cv.archives-ouvertes.fr\/matthieu-moy\/\">List of publications<\/a>.<\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Alexandre Moine<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">Researcher at <a href=\"https:\/\/www.inria.fr\/\">Inria<\/a>.<br>Keywords: formal verification, compilation, programming languages, Rocq.<br>Home page: <a href=\"https:\/\/alexandremoine.fr\">https:\/\/alexandremoine.fr<\/a>, <a href=\"https:\/\/cv.hal.science\/alexandre-moine\">List of publications<\/a><\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Gabriel Radanne<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">Researcher at <a href=\"https:\/\/www.inria.fr\/\">Inria<\/a>.<br>Keywords: programming languages, type systems, meta-programming<br>Home page: <a href=\"https:\/\/gabriel.radanne.net\/\">https:\/\/gabriel.radanne.net\/<\/a>, <a href=\"https:\/\/cv.archives-ouvertes.fr\/gabriel-radanne\">List of publications<\/a>.<\/p>\n\n\n\n<h1 class=\"wp-block-heading\">Associated Member<\/h1>\n\n\n\n<h2 class=\"wp-block-heading\">Filippo Alberto Edoardo<br>Nuccio Mortarino Majno di Capriglio<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">Assistant professor at <a href=\"https:\/\/www.univ-st-etienne.fr\/fr\/index.html\">Universit\u00e9 Jean Monnet Saint-\u00c9tienne<\/a> CNRS UMR 5208, <a href=\"https:\/\/math.univ-lyon1.fr\/icj\/\">Institut Camille Jordan<\/a> et <a href=\"https:\/\/www.iut.univ-st-etienne.fr\/fr\/index.html\">IUT.<\/a><br>D\u00e9l\u00e9gation 2025-2026 at <a href=\"https:\/\/www.inria.fr\/\">Inria<\/a>.<br>Keywords: formalization of mathematics, number theory, mathlib, Lean<br>Home page: <a href=\"https:\/\/perso.univ-st-etienne.fr\/nf51454h\/index_eng.html\">https:\/\/perso.univ-st-etienne.fr\/nf51454h\/index_eng.html<\/a><\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Yannick Zakowski<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">Researcher at <a href=\"https:\/\/www.inria.fr\/\">Inria<\/a>.<br>Keywords: semantics, verified compilation, proof assistants, Rocq.<br>Home page:&nbsp;<a href=\"https:\/\/cambium.inria.fr\/~yzakowsk\/\">https:\/\/cambium.inria.fr\/~yzakowsk\/<\/a><\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Laure Gonnord<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">Professor at Professor at Grenoble INP &amp; Verimag Lab<br>Keywords: abstract interpretation, compilation.<br>Home page: <a href=\"http:\/\/laure.gonnord.org\/pro\/\">http:\/\/laure.gonnord.org\/pro\/<\/a>, <a href=\"https:\/\/hal.archives-ouvertes.fr\/search\/index\/q\/%2A\/authIdHal_s\/laure-gonnord\/\">List of publications<\/a><\/p>\n\n\n\n<h1 class=\"wp-block-heading\">Post doc<\/h1>\n\n\n\n<p class=\"wp-block-paragraph\">None at the moment.<\/p>\n\n\n\n<h1 class=\"wp-block-heading\">Ph.D Students<\/h1>\n\n\n\n<ul class=\"wp-block-list\">\n<li>Alec Sadler (2023-)&nbsp;<a href=\"http:\/\/alsadler.github.io\">webpage<\/a><\/li>\n\n\n\n<li>Emma Nardino (2024-) <a href=\"https:\/\/perso.ens-lyon.fr\/emma.nardino\/\">webpage<\/a><\/li>\n\n\n\n<li>\u00c9tienne Parent (2025-)&nbsp;<a href=\"https:\/\/etienneparent.fr\/\">webpage<\/a><\/li>\n\n\n\n<li>Vivien Gachet (2025-)<\/li>\n\n\n\n<li>Gregoire Aubertin (2025-)<\/li>\n\n\n\n<li>Vincent Mastain (2025-)<\/li>\n\n\n\n<li>Samy Avrillon (2025-)<\/li>\n<\/ul>\n\n\n\n<h1 class=\"wp-block-heading\">Administrative staff<\/h1>\n\n\n\n<h2 class=\"wp-block-heading\">\u00c9lise Denoyelle<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">Inria.<\/p>\n\n\n\n<h1 class=\"wp-block-heading\">Past Post-doc:<\/h1>\n\n\n\n<ul class=\"wp-block-list\">\n<li>Bruno FERRES (2022-2023) <a href=\"https:\/\/ferres.me\/\">webpage<\/a><\/li>\n\n\n\n<li>Emmanuel Arrighi (2023-2024) <a href=\"https:\/\/emmanuel.arrighi.eu\/\">webpage<\/a><\/li>\n\n\n\n<li>Th\u00e9o Stoskopf (2024-2026) <a href=\"https:\/\/theostos.github.io\/\">webpage<\/a><\/li>\n\n\n\n<li>C\u00e9cile Marcon (2026)<\/li>\n<\/ul>\n\n\n\n<h1 class=\"wp-block-heading\">Past Ph.D students<\/h1>\n\n\n\n<ul class=\"wp-block-list\">\n<li>Paul Iannetta (2018-2022) <a href=\"https:\/\/pro.mizuga.me\/\">webpage<\/a><\/li>\n\n\n\n<li>Julien Braine (2018-2022)<\/li>\n\n\n\n<li>Julien Emmanuel (2019-2023) <a href=\"https:\/\/phd.julien-emmanuel.com\/\">webpage<\/a><\/li>\n\n\n\n<li>Amaury Maill\u00e9 (2019-2023) <a href=\"https:\/\/perso.ens-lyon.fr\/amaury.maille\/\">webpage<\/a><\/li>\n\n\n\n<li>Nicolas Chappe (2021-2024) <span class=\"user-profile-popover__heading\"><a href=\"https:\/\/www-verimag.imag.fr\/~chappen\/\">webpage<\/a><\/span><\/li>\n\n\n\n<li>Hugo <span class=\"user-profile-popover__heading\">Thievenaz (2021-2024)&nbsp;<\/span><a href=\"https:\/\/perso.ens-lyon.fr\/hugo.thievenaz\/\">webpage<\/a><\/li>\n\n\n\n<li>Tha\u00efs Baudon (2021-2024) <a href=\"http:\/\/perso.ens-lyon.fr\/thais.baudon\/\">webpage<\/a><\/li>\n\n\n\n<li>Oussama Oulkaid (2022-2025)<\/li>\n\n\n\n<li>Quentin Vermande (2023-2026) <a href=\"https:\/\/www.normalesup.org\/~qvermande\/index\">webpage<\/a><\/li>\n<\/ul>\n\n\n\n<p class=\"wp-block-paragraph\"><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Permanent Members Christophe Alias Researcher at Inria.Keywords: compilation, high-level synthesis, polyhedral model.Home page: http:\/\/perso.ens-lyon.fr\/christophe.alias\/, List of publications Aur\u00e8le Barri\u00e8re Researcher at CNRS.Keywords: formal verification, compilation, regular expressions, Rocq.Home page:&nbsp;https:\/\/aurele-barriere.github.io, List of publications Cyril Cohen Researcher at Inria.Keywords: proof assistants, type theory, Rocq, formalization of mathematics, mathcomp.Home page: http:\/\/cyrilcohen.fr, List of publications Ludovic Henrio (team co-leader) &hellip; <a href=\"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/?page_id=9\" class=\"more-link\">Continue reading<span class=\"screen-reader-text\"> &#8220;Members&#8221;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-9","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=\/wp\/v2\/pages\/9","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=9"}],"version-history":[{"count":45,"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=\/wp\/v2\/pages\/9\/revisions"}],"predecessor-version":[{"id":853,"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=\/wp\/v2\/pages\/9\/revisions\/853"}],"wp:attachment":[{"href":"https:\/\/www.ens-lyon.fr\/LIP\/CASH\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=9"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}