{"id":48,"date":"2019-03-11T09:32:55","date_gmt":"2019-03-11T08:32:55","guid":{"rendered":"http:\/\/lig-membres.imag.fr\/mechenim\/?p=48"},"modified":"2024-02-27T09:38:08","modified_gmt":"2024-02-27T08:38:08","slug":"welcome-2","status":"publish","type":"post","link":"https:\/\/lig-membres.imag.fr\/mechenim\/2019\/03\/11\/welcome-2\/","title":{"rendered":"Welcome!"},"content":{"rendered":"\r\n<p>I am a professor at <a href=\"http:\/\/ensimag.grenoble-inp.fr\/welcome\/\">Grenoble INP &#8211; Ensimag<\/a>. I obtained my PhD in 2005 under the supervision of Thierry Boy de la Tour and Ricardo Caferra, and received a PhD award from INPG. I did postdoctoral research at the University of Verona (Italy) under the supervision of <a href=\"http:\/\/profs.sci.univr.it\/~bonacina\/\">Maria Paola Bonacina<\/a> before being recruited at Ensimag. I defended my Habilitation thesis on Nov. 9th, 2017. The manuscript (in french) is available <a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2016\/05\/ManuscritHDR.pdf\">here<\/a>.<\/p>\r\n\r\n\r\n\r\n<p>I am mainly interested in automated reasoning, and have currently been working on:<\/p>\r\n\r\n\r\n\r\n<ul class=\"wp-block-list\">\r\n<li>Separation logic<\/li>\r\n<li>The certification of quantum properties<\/li>\r\n<li>The formalization of financial mathematics<\/li>\r\n<li>Automated theorem provers for solving SMT problems<\/li>\r\n<li>Finite instantiation methods<\/li>\r\n<li>Inductive reasoning<\/li>\r\n<li>Abductive reasoning<\/li>\r\n<\/ul>\r\n<p>I have recently been interested in the formalization of financial mathematics\u00a0using the proof assistant <a href=\"https:\/\/isabelle.in.tum.de\/\">Isabelle<\/a>. A zipped folder containing results about the formalization in Isabelle of the Cox-Ross-Rubinstein model can be found <a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2019\/05\/DiscretePricing.tar.gz\">here<\/a>, though it strongly recommended to get the theory files available on the <a href=\"https:\/\/www.isa-afp.org\/entries\/DiscretePricing.html\">Archive of Formal Proofs<\/a>.<\/p>\r\n\r\n\r\n\r\n<h2 class=\"wp-block-heading\">Publications<\/h2>\r\n\r\n\r\n\r\n<p>Below is an outdated list of publications. A more complete list is available <a href=\"https:\/\/cv.archives-ouvertes.fr\/mnacho-echenim\">here<\/a>.<br \/><strong>Journal proceedings<\/strong><\/p>\r\n\r\n\r\n\r\n<ul class=\"wp-block-list\">\r\n<li>Mnacho Echenim, Nicolas Peltier and Sophie Tourret. Prime Implicate Generation in Equational Logic. Journal of Artificial Intelligence Research, 2017 (<a href=\"https:\/\/doi.org\/10.1613\/jair.5481\">DOI<\/a>). <a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2019\/03\/JAIR2017.pdf\">Paper<\/a><\/li>\r\n<li>Mnacho Echenim and Nicolas Peltier. A Superposition Calculus for Abductive Reasoning. Journal of Automated Reasoning, 2016. <a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2016\/05\/EP14.pdf\">Paper<\/a><\/li>\r\n<li>Vincent Aravantinos, Mnacho Echenim, and Nicolas Peltier. A resolution calculus for first-order schemata. Fundamenta Informaticae, 125(2):101133, 2013. <a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2016\/05\/AEP_RFOS.pdf\">Paper<\/a><\/li>\r\n<li>Mnacho Echenim and Nicolas Peltier. Instantiation Schemes for Nested Theories. ACM Transactions on Computational Logic, 14(2):11, 2013. <a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2016\/05\/EP_TOCL.pdf\">Paper<\/a><\/li>\r\n<li>Mnacho Echenim and Nicolas Peltier. An instantiation scheme for satisfiability modulo theories. Journal of Automated Reasoning, 48(3), 2012. <a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2016\/05\/EP_IsSMT.pdf\">Paper<\/a><\/li>\r\n<\/ul>\r\n\r\n\r\n\r\n<p><strong>Conference and workshop proceedings<\/strong><\/p>\r\n\r\n\r\n\r\n<ul class=\"wp-block-list\">\r\n<li>M. Echenim, N. Peltier, and S. Tourret. Quantifier-Free Equational Logic and Prime Implicate Generation. CADE 25, 2015. <a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2016\/05\/EPT_Cade25.pdf\">Paper<\/a><\/li>\r\n<li>M. Echenim, N. Peltier, and S. Tourret. A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses. PAAR 2014. <a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2016\/05\/EPT_Paar14.pdf\">Paper<\/a><\/li>\r\n<li>M. Echenim, N. Peltier, and S. Tourret. A Rewriting Strategy to Generate Prime Implicates in Equational Logic. IJCAR 2014. <a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2016\/05\/EPT_Ijcar14.pdf\">Paper<\/a><\/li>\r\n<li>M. Echenim, N. Peltier, and S. Tourret. An approach to abductive reasoning in equational logic. IJCAI 2013. <a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2016\/05\/EPT_Ijcai13_Long.pdf\">Extended version<\/a><\/li>\r\n<\/ul>\r\n\r\n\r\n\r\n<h2 class=\"wp-block-heading\">Teaching<\/h2>\r\n\r\n\r\n\r\n<p>I have been co-head of the <a href=\"http:\/\/ensimag.grenoble-inp.fr\/curriculum\/financial-engineering-239540.kjsp?RH=1228477151490\">Financial Engineering department<\/a> at Ensimag since 2009. These past years, I have been in charge of the following classes:<\/p>\r\n\r\n\r\n\r\n<ul class=\"wp-block-list\">\r\n<li>Formal Language Theory (Bac + 3). A possibly outdated version of the course notes (in french) is available <a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2016\/05\/PolycopieTL1.pdf\">here<\/a>.<\/li>\r\n<li>Logic bases for Computer Science (Bac + 4). The course notes (in french) are available\u00a0<a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2016\/05\/PolycopieLogique.pdf\">here<\/a>. A couple of videos of the lectures (in french) are available below:\r\n<ul>\r\n<li>Resolution &#8211; <a href=\"https:\/\/videos.univ-grenoble-alpes.fr\/video\/12940-resolution-definitions\/\">video 1<\/a>, <a href=\"https:\/\/videos.univ-grenoble-alpes.fr\/video\/12968-resolution-correction-completude\/\">video 2<\/a>, <a href=\"https:\/\/videos.univ-grenoble-alpes.fr\/video\/12972-resolution-un-exemple\/\">video 3<\/a><\/li>\r\n<li>Equality &#8211; <a href=\"https:\/\/videos.univ-grenoble-alpes.fr\/video\/13200-egalite-introduction-axiomatisation\/\">video 1<\/a>, <a href=\"https:\/\/videos.univ-grenoble-alpes.fr\/video\/13202-egalite-correction-paramodulation\/\">video 2<\/a>, <a href=\"https:\/\/videos.univ-grenoble-alpes.fr\/video\/13203-egalite-cloture-de-congruence\/\">video 3<\/a>, <a href=\"https:\/\/videos.univ-grenoble-alpes.fr\/video\/13209-egalite-cloture-de-congruence-exemples\/\">video 4<\/a><\/li>\r\n<li>Satisfiability Modulo Theories &#8211; <a href=\"https:\/\/videos.univ-grenoble-alpes.fr\/video\/13370-satisfaisabilite-modulo-des-theories-introduction\/\">video 1<\/a>, <a href=\"https:\/\/videos.univ-grenoble-alpes.fr\/video\/13377-satisfaisabilite-modulo-des-theories-dpllt\/\">video 2<\/a><\/li>\r\n<li>Herbrand&#8217;s theorem &#8211; <a href=\"https:\/\/videos.univ-grenoble-alpes.fr\/video\/13578-theoreme-de-herbrand-introduction\/\">video 1<\/a>, <a href=\"https:\/\/videos.univ-grenoble-alpes.fr\/video\/13584-theoreme-de-herbrand-formules-universelles\/\">video 2<\/a><\/li>\r\n<\/ul>\r\n<\/li>\r\n<li>Systematic strategies with .NET (Bac + 5)<\/li>\r\n<\/ul>\r\n\r\n\r\n\r\n<h2 class=\"wp-block-heading\">Conferences on quantum computing<\/h2>\r\n<p>I am in charge of a series of four conferences that serve as an introduction to quantum computing (in french). These conferences are now part of the <em>Kal\u00e9idoscope<\/em> week at Grenoble INP and can be attended by any of the &gt;1700 students of the institute. The conference topics are the following:<\/p>\r\n<ul>\r\n<li>The basis of quantum computing (<a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2024\/02\/Fondements.pdf\">slides<\/a>)<\/li>\r\n<li>Quantum algorithms (by <a href=\"https:\/\/alastair-abbott.github.io\/\">Alastair Abbott<\/a>, <a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2024\/02\/Calcul.pdf\">slides<\/a>)<\/li>\r\n<li>Quantum information (by <a href=\"https:\/\/membres-lig.imag.fr\/mhalla\/\">Mehdi Mhalla<\/a>, <a href=\"http:\/\/lig-membres.imag.fr\/mechenim\/wp-content\/uploads\/sites\/219\/2024\/02\/Correction.pdf\">slides<\/a>)<\/li>\r\n<li>Technologies for the design of quantum computers (by Franck Balestro)<\/li>\r\n<\/ul>\r\n<h3>Contact Information<\/h3>\r\n\r\n\r\n\r\n<p>Office: LIG, B\u00e2timent IMAG. 700 avenue Centrale. 38401 St Martin d&#8217;H\u00e8res. FRANCE <br \/>Phone: +33 4 57 42 14 91 <br \/>Email: Mnacho (dot) Echenim (at) univ-grenoble-alpes (dot) fr<\/p>\r\n","protected":false},"excerpt":{"rendered":"<p>I am a professor at Grenoble INP &#8211; Ensimag. I obtained my PhD in 2005 under the supervision of Thierry [&hellip;]<\/p>\n","protected":false},"author":837,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"site-sidebar-layout":"default","site-content-layout":"","ast-site-content-layout":"","site-content-style":"default","site-sidebar-style":"default","ast-global-header-display":"","ast-banner-title-visibility":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","astra-migrate-meta-layouts":"default","ast-page-background-enabled":"default","ast-page-background-meta":{"desktop":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-opacity":"","overlay-gradient":""},"tablet":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-opacity":"","overlay-gradient":""},"mobile":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-opacity":"","overlay-gradient":""}},"ast-content-background-meta":{"desktop":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-opacity":"","overlay-gradient":""},"tablet":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-opacity":"","overlay-gradient":""},"mobile":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-opacity":"","overlay-gradient":""}},"footnotes":""},"categories":[1],"tags":[],"class_list":["post-48","post","type-post","status-publish","format-standard","hentry","category-non-classe"],"_links":{"self":[{"href":"https:\/\/lig-membres.imag.fr\/mechenim\/wp-json\/wp\/v2\/posts\/48","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/lig-membres.imag.fr\/mechenim\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/lig-membres.imag.fr\/mechenim\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/lig-membres.imag.fr\/mechenim\/wp-json\/wp\/v2\/users\/837"}],"replies":[{"embeddable":true,"href":"https:\/\/lig-membres.imag.fr\/mechenim\/wp-json\/wp\/v2\/comments?post=48"}],"version-history":[{"count":13,"href":"https:\/\/lig-membres.imag.fr\/mechenim\/wp-json\/wp\/v2\/posts\/48\/revisions"}],"predecessor-version":[{"id":77,"href":"https:\/\/lig-membres.imag.fr\/mechenim\/wp-json\/wp\/v2\/posts\/48\/revisions\/77"}],"wp:attachment":[{"href":"https:\/\/lig-membres.imag.fr\/mechenim\/wp-json\/wp\/v2\/media?parent=48"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/lig-membres.imag.fr\/mechenim\/wp-json\/wp\/v2\/categories?post=48"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/lig-membres.imag.fr\/mechenim\/wp-json\/wp\/v2\/tags?post=48"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}