/* Scripts for my professional web-site: http://www.di.ens.fr/~mine Copyright (C) Antoine Miné 2011. */ /* main menu */ var options = [ ["img", "antoine_mini.png", "80%", "" ], ["Antoine Miné", "", "", "" ], ["br"], ["Home", "Accueil", "index", "" ], ["News", "Nouvelles", "index", "#news" ], ["Research", "Recherche", "index", "#research" ], ["Habilitation", "Habilitation", "hdr/index", "", "" ], ["Ph.D", "Thèse", "these/index", "" ], ["Projects", "Projets", "projects", "" ], ["Conferences", "Conférences", "confs", "", ], ["Software", "Logiciels", "index", "#soft", ], ["Publications", "Publications", "publications", "", "important" ], ["Talks", "Exposés", "talks", "" ], ["Teaching", "Enseignement", "index", "#teach", ], ["Emulation", "Émulation", "emulation", "" ], ["Contact", "Contact", "index", "#contact" ], ["-"], /* ["SAS 2012", "", "http://www.sas2012.ens.fr", "", "important" ], ["SSCPS 2012", "", "http://www.sscps.net", ""], ["SAS 2013", "", "http://research.microsoft.com/en-us/events/sas2013/", ""], */ ["iFM 2014", "", "http://ifm2014.cs.unibo.it/", ""], ["MOVEP 2014", "", "http://movep14.irccyn.ec-nantes.fr/", ""], ["TAPAS 2014", "", "http://cs.au.dk/tapas2014", ""], ["TASE 2014", "", "http://www.nudt.edu.cn/tase2014", ""], ["POPL 2015", "", "http://popl.mpi-sws.org/2015/", ""], ["-"], ["MPRI 2-6 course (M2)", "Cours MPRI 2-6 (M2)", "http://www.di.ens.fr/~mine/enseignement/mpri/2013-2014", ""], ["Semantic course (L3)", "Cours de sémantique (L3)", "http://www.di.ens.fr/~rival/semverif-2014/", ""], ["-"], ["AstréeA", "", "http://www.astreea.ens.fr", "", "important" ], ["Astrée", "", "http://www.astree.ens.fr", "" ], ["Apron", "", "http://apron.cri.ensmp.fr/library", "" ], ["-"], ["br"], ["img", "logo-cnrs.png", "64", "http://www.cnrs.fr" ], ["br"], ["img", "logo-ens.png", "82", "http://www.ens.fr" ], ["br"], ["img", "logo-inria.png", "128", "http://www.inria.fr" ], ]; function print_menu(base,here) { for (var i=0; i\n"); else if (options[i][0] == "br") document.write("
\n"); else if (options[i][0] == "img") { document.write("
"); if (options[i][3] != "") document.write(""); document.write("\"[""); if (options[i][3] != "") document.write(""); document.write("
\n"); } else { document.write("
"); var url = options[i][2]; if (url != "" && url.indexOf(".") == -1) url = url + ".html." + lang + options[i][3]; if (url != "" && url.indexOf(":") == -1) url = base + url; if (options[i][0] == here || url=="") document.write(""); else if (4 in options[i]) document.write(""); else document.write(""); document.write(options[i][ options[i][1]=="" || lang!="fr" ? 0 : 1]); if (options[i][0] == here || url=="") document.write(""); else document.write(""); document.write("
\n"); } } } function print_ref(s) { document.write(""); document.write("[" + s + "]"); document.write(""); } function mailchar(m,i) { var c = ""; switch (i) { case 0: c = 'm'; break; case 1: c = 'i'; break; case 2: c = 'n'; break; case 3: c = 'e'; break; case 4: c = '@'; break; case 5: c = 'd'; break; case 6: c = 'i'; break; case 7: c = '.'; break; case 8: c = 'e'; break; case 9: c = 'n'; break; case 10: c = 's'; break; case 11: c = '.'; break; case 12: c = 'f'; break; case 13: c = 'r'; break; } if (c != "") m.innerHTML = m.innerHTML + "" + c + ""; if (i<13) setTimeout(function () { mailchar(m,i+1); }, 100 + 100 * Math.random()); } function main() { var m = document.getElementsByName("mail"); for (var i=0; i