|
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"> |
|
2 <html> |
|
3 <head> |
|
4 <title>ITP 2015 in Nanjing</title> |
|
5 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> |
|
6 <style type="text/css"> |
|
7 #map_canvas { |
|
8 width: 500px; |
|
9 height: 400px; |
|
10 } |
|
11 </style> |
|
12 <script type="text/javascript" src="https://maps.googleapis.com/maps/api/js?sensor=false"></script> |
|
13 <script type="text/javascript"> |
|
14 function initialize() { |
|
15 var Latlng = new google.maps.LatLng(32.060255, 118.796877); |
|
16 var map_canvas = document.getElementById('map_canvas'); |
|
17 var map_options = { |
|
18 center: Latlng, |
|
19 zoom: 0, |
|
20 mapTypeId: google.maps.MapTypeId.HYBRID |
|
21 } |
|
22 var map = new google.maps.Map(map_canvas, map_options) |
|
23 |
|
24 var marker = new google.maps.Marker({ |
|
25 position: Latlng, |
|
26 map: map, |
|
27 title: 'Nanjing' |
|
28 }); |
|
29 } |
|
30 google.maps.event.addDomListener(window, 'load', initialize); |
|
31 </script> |
|
32 <style type="text/css"> |
|
33 body { font-size: 14px; |
|
34 font-family: "trebuchet ms", helvetica, sans-serif; } |
|
35 </style> |
|
36 </head> |
|
37 |
|
38 <BODY TEXT="#000000" |
|
39 BGCOLOR="#4169E1" |
|
40 LINK="#0000EF" |
|
41 VLINK="#51188E" |
|
42 ALINK="#FF0000" |
|
43 onload="initialize()" onunload="GUnload()"> |
|
44 |
|
45 <TABLE WIDTH="100%" |
|
46 BGCOLOR="#4169E1" |
|
47 BORDER="0" |
|
48 FRAME="border" |
|
49 CELLPADDING="10" |
|
50 CELLSPACING="2" |
|
51 RULES="all"> |
|
52 |
|
53 <!-- left column --> |
|
54 <TR> |
|
55 <TD BGCOLOR="#FFFFFF" |
|
56 WIDTH="20%" |
|
57 VALIGN="TOP" |
|
58 ROWSPAN="2"> |
|
59 |
|
60 |
|
61 <p align=center> |
|
62 <a href="pics/ITP-Linggusu.jpg"> |
|
63 <img src="pics/ITP-Linggusu.jpg" width="50%" height="12%" alt="Linggusi" border=0></a> |
|
64 <br> |
|
65 Linggusi pagoda<br> |
|
66 </p> |
|
67 |
|
68 <p align=center> |
|
69 <a href="pics/ITP-Mochou.jpg"> |
|
70 <img src="pics/ITP-Mochou.jpg" alt="Mochou" width="88%" height="18%" border=0></a> |
|
71 <br> |
|
72 Mochou Lake Park<br> |
|
73 </p> |
|
74 |
|
75 <p align=center> |
|
76 <a href="pics/ITP-najing-cit-walk.jpg"> |
|
77 <img src="pics/ITP-najing-cit-walk.jpg" alt="City Wall" width="50%" height="18%" border=0></a> |
|
78 <br> |
|
79 Nanjing city wall<br> |
|
80 </p> |
|
81 |
|
82 <p align=center> |
|
83 <a href="pics/Nanjing2.jpg"> |
|
84 <img src="pics/Nanjing2.jpg" alt="City Wall" width="80%" height="13%" border=0></a> |
|
85 <br> |
|
86 "Elephant Road" of the<br> Ming tomb<br> |
|
87 </p> |
|
88 |
|
89 <p align=center> |
|
90 <a href="pics/Nanjing3.jpg"> |
|
91 <img src="pics/Nanjing3.jpg" alt="Nanjing's skyline" width="80%" height="13%" border=0></a> |
|
92 <br> |
|
93 Nanjing's skyline<br> |
|
94 </p> |
|
95 |
|
96 <p align=center> |
|
97 <a href="pics/Nanjing4.jpg"> |
|
98 <img src="pics/Nanjing4.jpg" alt="Science and Technology Museum" width="80%" height="18%" border=0></a> |
|
99 <br> |
|
100 Science and Technology<br> Museum<br> |
|
101 </p> |
|
102 |
|
103 </TD> |
|
104 |
|
105 |
|
106 <!-- right column --> |
|
107 <TD BGCOLOR="#FFFFFF" WIDTH="75%" VALIGN="TOP"> |
|
108 <TABLE> |
|
109 <TR> |
|
110 <TD><H1>ITP Heritage</H1></TD> |
|
111 </TABLE> |
|
112 <p> |
|
113 [CFP] |
|
114 [<A HREF="history.html">Conference History</A>] |
|
115 </p> |
|
116 |
|
117 <p>ITP 2015 is the sixth conference on Interactive Theorem Proving and |
|
118 related topics, ranging from theoretical foundations to implementation |
|
119 aspects and applications in program verification, security, and |
|
120 formalization of mathematics. The inaugural meeting of ITP was held on |
|
121 11-14 July 2010 in Edinburgh, Scotland, as part of the Federated Logic |
|
122 Conference (FLoC, 9-21 July 2010). ITP is the evolution of the TPHOLs |
|
123 conference series to the broad field of interactive theorem |
|
124 proving. TPHOLs meetings took place every year from 1988 until 2009. |
|
125 </p> |
|
126 |
|
127 <h3>The TPHOLs conference series</h3> |
|
128 |
|
129 <p>TPHOLs 2009 was the twenty-second in a series of international |
|
130 conferences on the applications of higher order logic theorem proving. |
|
131 The first three (two at Cambridge and one at Århus) were informal |
|
132 users' meetings for the HOL system and were the only ones without |
|
133 published papers. Between 1991 and 1995 (Davis, Leuven, Vancouver, |
|
134 Malta, Utah) the conference entertained an increasingly wide field of |
|
135 interest. </p> |
|
136 |
|
137 <p>The evolution resulted in the program committee for the meeting in |
|
138 Turku (1996) deeming that the scope of the conference included all |
|
139 reasoning tools for higher order logics and adopted the name TPHOLs, |
|
140 being an acronym for Theorem Proving in Higher Order Logics. (The |
|
141 final letter being considered necessary to break the direct connection |
|
142 between the conference and the HOL system.) This decision was strongly |
|
143 endorsed at the business sessions at Turku and Murray Hill (1997). |
|
144 </p> |
|
145 |
|
146 <p>An extensive collection of links to various aspects of previous |
|
147 conferences in the series may be found below. </p> |
|
148 |
|
149 <h3>Associated communities</h3> |
|
150 <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> |
|
151 |
|
152 <a class='urllink' href='http://abella.cs.umn.edu' rel='nofollow'>Abella</a> - |
|
153 <a class='urllink' href='http://wiki.portal.chalmers.se/agda/pmwiki.php' rel='nofollow'>Agda</a> - |
|
154 <a class='urllink' href='http://www.cs.utexas.edu/users/moore/acl2' rel='nofollow'>ACL2</a> - |
|
155 <a class='urllink' href='http://coq.inria.fr' rel='nofollow'>Coq</a> - |
|
156 <a class='urllink' href='http://www.cl.cam.ac.uk/research/hvg/HOL' rel='nofollow'>HOL</a> - |
|
157 <a class='urllink' href='http://imps.mcmaster.ca' rel='nofollow'>IMPS</a> - |
|
158 <a class='urllink' href='http://www.cl.cam.ac.uk/research/hvg/Isabelle' rel='nofollow'>Isabelle</a> - |
|
159 <a class='urllink' href='http://www.dcs.ed.ac.uk/home/lego' rel='nofollow'>LEGO</a> - |
|
160 <a class='urllink' href='http://matita.cs.unibo.it' rel='nofollow'>Matita</a> - |
|
161 <a class='urllink' href='http://www.nuprl.org' rel='nofollow'>Nuprl</a> - |
|
162 <a class='urllink' href='http://www.lemma-one.com/ProofPower/index/index.html' rel='nofollow'>ProofPower</a> - |
|
163 <a class='urllink' href='http://pvs.csl.sri.com' rel='nofollow'>PVS</a> - |
|
164 </p> |
|
165 |
|
166 <h3>Traditions</h3> |
|
167 |
|
168 <p>A longstanding convention is that the annual conference should be |
|
169 held in a continent different to the location of the previous meeting. |
|
170 Another tradition is that the organizers for each meeting handle all |
|
171 aspects of the conference for the whole year in consultation with the |
|
172 previous few organizers. This includes selection of the programme |
|
173 committee, editing the proceedings, fund-raising, programme and local |
|
174 arrangements. Another responsibility of the organizers in year n is to |
|
175 call for bids and conduct a poll for the selection of the venue for |
|
176 the conference in year n+1. </p> |
|
177 |
|
178 <h3>ITP and TPHOLs conferences</h3> |
|
179 |
|
180 <table border='1'> |
|
181 <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, |
|
182 associated with FloC and the Vienna Summer of Logic.</td></tr> |
|
183 |
|
184 <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> |
|
185 |
|
186 <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> |
|
187 |
|
188 <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> |
|
189 |
|
190 <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> |
|
191 |
|
192 <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> |
|
193 |
|
194 <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> |
|
195 |
|
196 <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> |
|
197 |
|
198 <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> |
|
199 |
|
200 <tr ><td >2005</td><td >The 18th International Conference on Theorem Proving in Higher Order Logics, Oxford, UK , 22-25 August 2005.</td></tr> |
|
201 |
|
202 <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> |
|
203 |
|
204 <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> |
|
205 |
|
206 <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> |
|
207 |
|
208 <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> |
|
209 <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> |
|
210 |
|
211 <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> |
|
212 |
|
213 <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> |
|
214 |
|
215 <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> |
|
216 |
|
217 <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> |
|
218 |
|
219 <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> |
|
220 |
|
221 <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> |
|
222 |
|
223 <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> |
|
224 |
|
225 <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> |
|
226 |
|
227 <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> |
|
228 |
|
229 <tr ><td >1990</td><td >The 3rd International HOL Users Meeting, Aarhus University, Denmark, 1-2 October 1990.</td></tr> |
|
230 |
|
231 <tr ><td >1989</td><td >The 2nd International HOL Users Meeting, Trinity Hall, Cambridge, 14-15 December 1989.</td></tr> |
|
232 |
|
233 <tr ><td >1988</td><td >The 1st International HOL Users Meeting, Sidney Sussex College, Cambridge, 29-30 September 1988.</td></tr> |
|
234 |
|
235 </table> |
|
236 |
|
237 </TD> |
|
238 </TR> |
|
239 </TABLE> |
|
240 |
|
241 <hr> |
|
242 <a href="http://validator.w3.org/check/referer">[Validate this page.]</a> |
|
243 </body> |
|
244 </html> |