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 |
<script type="text/javascript" src="https://maps.googleapis.com/maps/api/js?sensor=false"></script>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
13 |
<script type="text/javascript">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
14 |
function initialize() {
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
15 |
var Latlng = new google.maps.LatLng(32.060255, 118.796877);
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
16 |
var map_canvas = document.getElementById('map_canvas');
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
17 |
var map_options = {
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
18 |
center: Latlng,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
19 |
zoom: 0,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
20 |
mapTypeId: google.maps.MapTypeId.HYBRID
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
21 |
}
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
22 |
var map = new google.maps.Map(map_canvas, map_options)
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
23 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
24 |
var marker = new google.maps.Marker({
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
25 |
position: Latlng,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
26 |
map: map,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
27 |
title: 'Nanjing'
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
28 |
});
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
29 |
}
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
30 |
google.maps.event.addDomListener(window, 'load', initialize);
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
31 |
</script>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
32 |
<style type="text/css">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
33 |
body { font-size: 14px;
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
34 |
font-family: "trebuchet ms", helvetica, sans-serif; }
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
35 |
</style>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
36 |
</head>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
37 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
38 |
<BODY TEXT="#000000"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
39 |
BGCOLOR="#4169E1"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
40 |
LINK="#0000EF"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
41 |
VLINK="#51188E"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
42 |
ALINK="#FF0000"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
43 |
onload="initialize()" onunload="GUnload()">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
44 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
45 |
<TABLE WIDTH="100%"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
46 |
BGCOLOR="#4169E1"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
47 |
BORDER="0"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
48 |
FRAME="border"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
49 |
CELLPADDING="10"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
50 |
CELLSPACING="2"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
51 |
RULES="all">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
52 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
53 |
<!-- left column -->
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
54 |
<TR>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
55 |
<TD BGCOLOR="#FFFFFF"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
56 |
WIDTH="20%"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
57 |
VALIGN="TOP"
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
58 |
ROWSPAN="2">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
59 |
|
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/ITP-Linggusu.jpg">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
63 |
<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
|
64 |
<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
65 |
Linggusi pagoda<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/ITP-Mochou.jpg">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
70 |
<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
|
71 |
<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
72 |
Mochou Lake Park<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/ITP-najing-cit-walk.jpg">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
77 |
<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
|
78 |
<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
79 |
Nanjing city wall<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 |
<p align=center>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
83 |
<a href="pics/Nanjing2.jpg">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
84 |
<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
|
85 |
<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
86 |
"Elephant Road" of the<br> Ming tomb<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
87 |
</p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
88 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
89 |
<p align=center>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
90 |
<a href="pics/Nanjing3.jpg">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
91 |
<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
|
92 |
<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
93 |
Nanjing's skyline<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
94 |
</p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
95 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
96 |
<p align=center>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
97 |
<a href="pics/Nanjing4.jpg">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
98 |
<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
|
99 |
<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
100 |
Science and Technology<br> Museum<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
101 |
</p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
102 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
103 |
</TD>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
104 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
105 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
106 |
<!-- right column -->
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
107 |
<TD BGCOLOR="#FFFFFF" WIDTH="75%" VALIGN="TOP">
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
108 |
<TABLE>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
109 |
<TR>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
110 |
<TD><H1>ITP Heritage and Conference History</H1></TD>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
111 |
</TABLE>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
112 |
<p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
113 |
<HR>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
114 |
[<A HREF="index.html">Home</A>]
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
115 |
[<A HREF="index.html#dates">Important Dates</A>]
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
116 |
[<A HREF="cfp.pdf">CFP</A>]
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
117 |
[<A HREF="index.html#committees">Committees</A>]
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
118 |
[<A HREF="history.html">Conference History</A>]
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
119 |
<HR>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
120 |
</p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
121 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
122 |
<p>ITP 2015 is the sixth conference on Interactive Theorem Proving and
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
123 |
related topics, ranging from theoretical foundations to implementation
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
124 |
aspects and applications in program verification, security, and
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
125 |
formalization of mathematics. The inaugural meeting of ITP was held on
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
126 |
11-14 July 2010 in Edinburgh, Scotland, as part of the Federated Logic
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
127 |
Conference (FLoC, 9-21 July 2010). ITP is the evolution of the TPHOLs
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
128 |
conference series to the broad field of interactive theorem
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
129 |
proving. TPHOLs meetings took place every year from 1988 until 2009.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
130 |
</p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
131 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
132 |
<h3>The TPHOLs conference series</h3>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
133 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
134 |
<p>TPHOLs 2009 was the twenty-second in a series of international
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
135 |
conferences on the applications of higher order logic theorem proving.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
136 |
The first three (two at Cambridge and one at Århus) were informal
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
137 |
users' meetings for the HOL system and were the only ones without
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
138 |
published papers. Between 1991 and 1995 (Davis, Leuven, Vancouver,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
139 |
Malta, Utah) the conference entertained an increasingly wide field of
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
140 |
interest. </p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
141 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
142 |
<p>The evolution resulted in the program committee for the meeting in
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
143 |
Turku (1996) deeming that the scope of the conference included all
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
144 |
reasoning tools for higher order logics and adopted the name TPHOLs,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
145 |
being an acronym for Theorem Proving in Higher Order Logics. (The
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
146 |
final letter being considered necessary to break the direct connection
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
147 |
between the conference and the HOL system.) This decision was strongly
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
148 |
endorsed at the business sessions at Turku and Murray Hill (1997).
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
149 |
</p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
150 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
151 |
<p>An extensive collection of links to various aspects of previous
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
152 |
conferences in the series may be found below. </p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
153 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
154 |
<h3>Associated communities</h3>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
155 |
<p>An inspection of the proceedings of recent conferences show that the conference accommodates the user communities of a number of theorem proving systems that support higher order logics. The interested reader is referred to the web sites for the following provers:<br>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
156 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
157 |
<a class='urllink' href='http://abella.cs.umn.edu' rel='nofollow'>Abella</a> -
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
158 |
<a class='urllink' href='http://wiki.portal.chalmers.se/agda/pmwiki.php' rel='nofollow'>Agda</a> -
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
159 |
<a class='urllink' href='http://www.cs.utexas.edu/users/moore/acl2' rel='nofollow'>ACL2</a> -
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
160 |
<a class='urllink' href='http://coq.inria.fr' rel='nofollow'>Coq</a> -
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
161 |
<a class='urllink' href='http://www.cl.cam.ac.uk/research/hvg/HOL' rel='nofollow'>HOL</a> -
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
162 |
<a class='urllink' href='http://imps.mcmaster.ca' rel='nofollow'>IMPS</a> -
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
163 |
<a class='urllink' href='http://www.cl.cam.ac.uk/research/hvg/Isabelle' rel='nofollow'>Isabelle</a> -
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
164 |
<a class='urllink' href='http://www.dcs.ed.ac.uk/home/lego' rel='nofollow'>LEGO</a> -
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
165 |
<a class='urllink' href='http://matita.cs.unibo.it' rel='nofollow'>Matita</a> -
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
166 |
<a class='urllink' href='http://www.nuprl.org' rel='nofollow'>Nuprl</a> -
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
167 |
<a class='urllink' href='http://www.lemma-one.com/ProofPower/index/index.html' rel='nofollow'>ProofPower</a> -
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
168 |
<a class='urllink' href='http://pvs.csl.sri.com' rel='nofollow'>PVS</a> -
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
169 |
</p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
170 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
171 |
<h3>Traditions</h3>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
172 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
173 |
<p>A longstanding convention is that the annual conference should be
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
174 |
held in a continent different to the location of the previous meeting.
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
175 |
Another tradition is that the organizers for each meeting handle all
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
176 |
aspects of the conference for the whole year in consultation with the
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
177 |
previous few organizers. This includes selection of the programme
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
178 |
committee, editing the proceedings, fund-raising, programme and local
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
179 |
arrangements. Another responsibility of the organizers in year n is to
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
180 |
call for bids and conduct a poll for the selection of the venue for
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
181 |
the conference in year n+1. </p>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
182 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
183 |
<h3>ITP and TPHOLs conferences</h3>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
184 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
185 |
<table border='1'>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
186 |
<tr><td >2014</td><td ><a class='urllink' href='http://www.cs.uwyo.edu/~ruben/itp-2014/' rel='nofollow'>5th International Conference on Interactive Theorem Proving</a>, Vienna, Austria, July 14-17, 2014,
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
187 |
associated with FloC and the Vienna Summer of Logic.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
188 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
189 |
<tr><td >2013</td><td ><a class='urllink' href='http://itp2013.inria.fr' rel='nofollow'>4th International Conference on Interactive Theorem Proving</a>, Rennes, France, July 22-26, 2013</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
190 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
191 |
<tr ><td >2012</td><td ><a class='urllink' href='http://itp2012.cs.princeton.edu' rel='nofollow'>3rd International Conference on Interactive Theorem Proving</a>, Princeton, NJ, US, August 13-15 2012</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
192 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
193 |
<tr ><td >2011</td><td ><a class='urllink' href='http://itp2011.cs.ru.nl/ITP2011/Home.html' rel='nofollow'>2nd International Conference on Interactive Theorem Proving</a>, The Netherlands, August 22-25 2011</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
194 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
195 |
<tr ><td >2010</td><td ><a class='urllink' href='http://www.floc-conference.org/ITP-home.html' rel='nofollow'>1st International Conference on Interactive Theorem Proving</a>, Edinburgh, Scotland, July 11-14, 2010</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
196 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
197 |
<tr ><td >2009</td><td ><a class='urllink' href='http://isabelle.in.tum.de/nominal/activities/tphols09/' rel='nofollow'>The 22nd International Conference on Theorem Proving in Higher Order Logics</a>, Munich, Germany, August 17-20, 2009.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
198 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
199 |
<tr ><td >2008</td><td ><a class='urllink' href='http://users.encs.concordia.ca/%7Etphols08/TPHOLs2008/' rel='nofollow'>The 21th International Conference on Theorem Proving in Higher Order Logics</a>, Montreal, Canada, August 18-21, 2008.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
200 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
201 |
<tr ><td >2007</td><td ><a class='urllink' href='http://rsg.informatik.uni-kl.de/TPHOLs-2007/' rel='nofollow'>The 20th International Conference on Theorem Proving in Higher Order Logics</a>, Kaiserslautern, Germany, September 10-13, 2007.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
202 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
203 |
<tr ><td >2006</td><td >The 19th International Conference on Theorem Proving in Higher Order Logics merged with FloC, Seattle, August 17-20, 2006.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
204 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
205 |
<tr ><td >2005</td><td >The 18th International Conference on Theorem Proving in Higher Order Logics, Oxford, UK , 22-25 August 2005.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
206 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
207 |
<tr ><td >2004</td><td ><a class='urllink' href='http://www.cs.utah.edu/tphols2004' rel='nofollow'>The 17th International Conference on Theorem Proving in Higher Order Logics</a>, Park City, Utah, USA, 14-17 September 2004.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
208 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
209 |
<tr ><td >2003</td><td ><a class='urllink' href='http://tphols.informatik.uni-freiburg.de/' rel='nofollow'>The 16th International Conference on Theorem Proving in Higher Order Logics</a>, Rome, Italy, 9-12 September 2003.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
210 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
211 |
<tr ><td >2002</td><td >The 15th International Conference on Theorem Proving in Higher Order Logics, Hampton, Virginia, USA, 20-23 August 2002.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
212 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
213 |
<tr ><td >2001</td><td ><a class='urllink' href='http://www.dcs.gla.ac.uk/TPHOLs2001/' rel='nofollow'>The 14th International Conference on Theorem Proving in Higher Order Logics</a>, Edinburgh, Scotland, 3-6 September 2001.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
214 |
<tr ><td >2000</td><td >The 13th International Conference on Theorem Proving in Higher Order Logics, Portland, Oregon, USA, 14-18 August 2000.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
215 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
216 |
<tr ><td >1999</td><td >The 12th International Conference on Theorem Proving in Higher Order Logics, Unversity of Nice-Sophia-Antipolis, Nice, France, 14-17 September 1999.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
217 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
218 |
<tr ><td >1998</td><td ><a class='urllink' href='http://cs.anu.edu.au/TPHOLs98/' rel='nofollow'>The 11th International Conference on Theorem Proving in Higher Order Logics</a>, The Australian National University, Canberra, Australia, 28 September - 1 October 1998.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
219 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
220 |
<tr ><td >1997</td><td >The 10th International Conference on Theorem Proving in Higher Order Logics, Bell Labs, Murray Hill, New Jersey, USA, 19-22 August 1997.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
221 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
222 |
<tr ><td >1996</td><td >The 9th International Conference on Theorem Proving in Higher Order Logics, Turku Center for Computer Science and Åbo Akademi University, Turku, Finland, 26-30 August 1996.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
223 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
224 |
<tr ><td >1995</td><td >The 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, Aspen Grove, Utah, USA, 11-14 September 1995.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
225 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
226 |
<tr ><td >1994</td><td >The 7th International Workshop on Higher Order Logic Theorem Proving and its Applications, Valletta, Malta, 19-22 September 1994.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
227 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
228 |
<tr ><td >1993</td><td >The 6th International Workshop on Higher Order Logic Theorem Proving and its Applications, Vancouver, B.C., Canada, 10-13 August 1993.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
229 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
230 |
<tr ><td >1992</td><td >The 5th International Workshop on Higher Order Logic Theorem Proving and its Applications, IMEC, Leuven, Belgium, 21-24 September 1992.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
231 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
232 |
<tr ><td >1991</td><td >The 4th International Workshop on the HOL Theorem Proving System and its Applications, Davis, California, USA, 28-30 August 1991.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
233 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
234 |
<tr ><td >1990</td><td >The 3rd International HOL Users Meeting, Aarhus University, Denmark, 1-2 October 1990.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
235 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
236 |
<tr ><td >1989</td><td >The 2nd International HOL Users Meeting, Trinity Hall, Cambridge, 14-15 December 1989.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
237 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
238 |
<tr ><td >1988</td><td >The 1st International HOL Users Meeting, Sidney Sussex College, Cambridge, 29-30 September 1988.</td></tr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
239 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
240 |
</table>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
241 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
242 |
</TD>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
243 |
</TR>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
244 |
</TABLE>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
245 |
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
246 |
<hr>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
247 |
<a href="http://validator.w3.org/check/referer">[Validate this page.]</a>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
248 |
</body>
|
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
249 |
</html>
|