1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
/*
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<options.length; i++) {
if (options[i][0] == "-")
document.write("<div class=\"menuspace\"></div>\n");
else if (options[i][0] == "br")
document.write("<br>\n");
else if (options[i][0] == "img") {
document.write("<div class=\"icon\">");
if (options[i][3] != "")
document.write("<a href=\"" + options[i][3] + "\" class=\"noborder\">");
document.write("<img src=\"" + base + options[i][1] + "\" alt=\"[" +
options[i][1] + "]\" width=\"" + options[i][2] + "\">");
if (options[i][3] != "")
document.write("</a>");
document.write("</div>\n");
}
else {
document.write("<div class=\"menuitem\">");
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("<b>");
else if (4 in options[i]) document.write("<a href=\"" + url + "\" class=\"" + options[i][4] + "\">");
else document.write("<a href=\"" + url + "\">");
document.write(options[i][ options[i][1]=="" || lang!="fr" ? 0 : 1]);
if (options[i][0] == here || url=="") document.write("</b>");
else document.write("</a>");
document.write("</div>\n");
}
}
}
function print_ref(s)
{
document.write("<a href=\"publications.html." + lang + "#" + s + "\">");
document.write("<span class=\"pref\">[" + s + "]</span>");
document.write("</a>");
}
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 + "<span>" + c + "</span>";
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<m.length; i++) {
mailchar(m[i],0);
}
}
|
