itp-2015: bids-2016.html@af0ecdcd08a9 (annotated)

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

author	Christian Urban <christian.urban@kcl.ac.uk>
	Sat, 11 Apr 2015 04:27:31 +0100 (2015-04-11)
changeset 115	af0ecdcd08a9
child 117	7ea39721aea7
permissions	-rw-r--r--