115
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
1 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
2 |
<html>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
3 |
<head>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
4 |
<title>ITP 2015 in Nanjing</title>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
5 |
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
6 |
<style type="text/css">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
7 |
#map_canvas {
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
8 |
width: 500px;
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
9 |
height: 400px;
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
10 |
}
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
11 |
</style>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
12 |
<style type="text/css">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
13 |
body { font-size: 14px;
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
14 |
font-family: "trebuchet ms", helvetica, sans-serif; }
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
15 |
</style>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
16 |
</head>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
17 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
18 |
<BODY TEXT="#000000"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
19 |
BGCOLOR="#4169E1"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
20 |
LINK="#0000EF"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
21 |
VLINK="#51188E"
|
119
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
22 |
ALINK="#FF0000">
|
115
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
23 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
24 |
<TABLE WIDTH="100%"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
25 |
BGCOLOR="#4169E1"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
26 |
BORDER="0"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
27 |
FRAME="border"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
28 |
CELLPADDING="10"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
29 |
CELLSPACING="2"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
30 |
RULES="all">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
31 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
32 |
<!-- left column -->
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
33 |
<TR>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
34 |
<TD BGCOLOR="#FFFFFF"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
35 |
WIDTH="20%"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
36 |
VALIGN="TOP"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
37 |
ROWSPAN="2">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
38 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
39 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
40 |
<p align=center>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
41 |
<a href="pics/ITP-Linggusu.jpg">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
42 |
<img src="pics/ITP-Linggusu.jpg" width="50%" height="12%" alt="Linggusi" border=0></a>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
43 |
<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
44 |
Linggusi pagoda<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
45 |
</p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
46 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
47 |
<p align=center>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
48 |
<a href="pics/ITP-Mochou.jpg">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
49 |
<img src="pics/ITP-Mochou.jpg" alt="Mochou" width="88%" height="18%" border=0></a>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
50 |
<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
51 |
Mochou Lake Park<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
52 |
</p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
53 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
54 |
<p align=center>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
55 |
<a href="pics/ITP-najing-cit-walk.jpg">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
56 |
<img src="pics/ITP-najing-cit-walk.jpg" alt="City Wall" width="50%" height="18%" border=0></a>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
57 |
<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
58 |
Nanjing city wall<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
59 |
</p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
60 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
61 |
<p align=center>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
62 |
<a href="pics/Nanjing2.jpg">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
63 |
<img src="pics/Nanjing2.jpg" alt="City Wall" width="80%" height="13%" border=0></a>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
64 |
<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
65 |
"Elephant Road" of the<br> Ming tomb<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
66 |
</p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
67 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
68 |
<p align=center>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
69 |
<a href="pics/Nanjing3.jpg">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
70 |
<img src="pics/Nanjing3.jpg" alt="Nanjing's skyline" width="80%" height="13%" border=0></a>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
71 |
<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
72 |
Nanjing's skyline<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
73 |
</p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
74 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
75 |
<p align=center>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
76 |
<a href="pics/Nanjing4.jpg">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
77 |
<img src="pics/Nanjing4.jpg" alt="Science and Technology Museum" width="80%" height="18%" border=0></a>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
78 |
<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
79 |
Science and Technology<br> Museum<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
80 |
</p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
81 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
82 |
</TD>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
83 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
84 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
85 |
<!-- right column -->
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
86 |
<TD BGCOLOR="#FFFFFF" WIDTH="75%" VALIGN="TOP">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
87 |
<TABLE>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
88 |
<TR>
|
117
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
89 |
<TD><H1>Bids for Hosting ITP 2016</H1></TD>
|
115
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
90 |
</TABLE>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
91 |
<p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
92 |
<HR>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
93 |
[<A HREF="index.html">Home</A>]
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
94 |
[<A HREF="index.html#dates">Important Dates</A>]
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
95 |
[<A HREF="cfp.pdf">CFP</A>]
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
96 |
[<A HREF="index.html#committees">Committees</A>]
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
97 |
[<A HREF="history.html">Conference History</A>]
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
98 |
<HR>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
99 |
</p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
100 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
101 |
<p>ITP 2015 is the sixth conference on Interactive Theorem Proving and
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
102 |
related topics, ranging from theoretical foundations to implementation
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
103 |
aspects and applications in program verification, security, and
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
104 |
formalization of mathematics. The inaugural meeting of ITP was held on
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
105 |
11-14 July 2010 in Edinburgh, Scotland, as part of the Federated Logic
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
106 |
Conference (FLoC, 9-21 July 2010). ITP is the evolution of the TPHOLs
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
107 |
conference series to the broad field of interactive theorem
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
108 |
proving. TPHOLs meetings took place every year from 1988 until 2009.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
109 |
</p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
110 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
111 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
112 |
</TD>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
113 |
</TR>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
114 |
</TABLE>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
115 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
116 |
<hr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
117 |
<a href="http://validator.w3.org/check/referer">[Validate this page.]</a>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
118 |
</body>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
119 |
</html>
|