Mercurial Mercurial > hg > itp-2015 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Mon, 18 May 2015 16:25:51 +0100
changeset 131 a5c905a33751
parent 130 9fa7b47fd6d7
child 132 1e45c648d484
updated
accepted.html file | annotate | diff | comparison | revisions
bids-2016.html file | annotate | diff | comparison | revisions
history.html file | annotate | diff | comparison | revisions
index.html file | annotate | diff | comparison | revisions 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/accepted.html	Mon May 18 16:25:51 2015 +0100
@@ -0,0 +1,11 @@
+<!DOCTYPE html
+      PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+      "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<html lang="en-US" xmlns="http://www.w3.org/1999/xhtml" xml:lang="en-US" style="display:none">
+<head>
+<title>ITP 2015 Accepted Papers</title>
+<script>window['ec:pageId']='11624752626377228288'</script>
+<meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
+<script>if(self != top) {top.location = self.location} else {document.documentElement.style.display = "block"}</script><script>if(self != top) {top.location = self.location}</script></head>
+<body><h1>ITP 2015 Accepted Papers</h1><style>.accepted {clear:right;margin-bottom:20pt;padding:3pt}</style><style>.abstract {border-left: solid black 1px;border-right: solid black 1px;border-top: solid black 1px;padding:3pt}</style><style>.paper {border-left: solid black 1px;border-right: solid black 1px;border-top: solid black 1px;padding:2pt}</style><style>.abstract:last-child {border-bottom: solid black 1px;padding:3pt}</style><style>.paper:last-child {border-bottom: solid black 1px;padding:2pt}</style><div class="paper"><span class="authors"><span><a href="http://www.infsec.ethz.ch/people/detail.html?persid=193410">Andreas Lochbihler</a> and Alexandra Maximova</span>. </span><span class="title">Stream Fusion for Isabelle’s Code Generator (Rough Diamond)</span></div><div class="paper"><span class="authors"><span><a href="http://tinyurl.com/lcfilipe">Luís Cruz-Filipe</a> and <a href="http://www.imada.sdu.dk/~petersk/">Peter Schneider-Kamp</a></span>. </span><span class="title">Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker</span></div><div class="paper"><span class="authors"><span>Bruno Barras, Carst Tankink and Enrico Tassi</span>. </span><span class="title">Asynchronous processing of Coq documents: from the kernel up to the user interface</span></div><div class="paper"><span class="authors"><a href="http://www.in.tum.de/~nipkow">Tobias Nipkow</a>. </span><span class="title">Amortized Complexity Verified</span></div><div class="paper"><span class="authors">Anthony Fox. </span><span class="title">Improved Tool Support for Machine-Code Decompilation in HOL4</span></div><div class="paper"><span class="authors"><span><a href="http://www-verimag.imag.fr/~boulme">Sylvain Boulmé</a> and Alexandre Maréchal</span>. </span><span class="title">Refinement to certify abstract interpretations, illustrated on linearization for polyhedra.</span></div><div class="paper"><span class="authors"><span>Arthur Charguéraud and François Pottier</span>. </span><span class="title">Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation</span></div><div class="paper"><span class="authors"><span><a href="http://www21.in.tum.de/~hoelzl/">Johannes Hölzl</a>, <a href="http://www.infsec.ethz.ch/people/detail.html?persid=193410">Andreas Lochbihler</a> and <a href="http://www21.in.tum.de/~traytel/">Dmitriy Traytel</a></span>. </span><span class="title">A Formalized Hierarchy of Probabilistic System Types (Proof Pearl)</span></div><div class="paper"><span class="authors"><span><a href="https://sites.google.com/site/petarmaksimovic1981/home">Petar Maksimovic</a> and <a href="http://www.irisa.fr/celtique/aschmitt/">Alan Schmitt</a></span>. </span><span class="title">HOCore in Coq</span></div><div class="paper"><span class="authors"><span><a href="http://people.cecs.anu.edu.au/user/4798">Hing-Lun Chan</a> and <a href="http://nicta.com.au/people/norrishm">Michael Norrish</a></span>. </span><span class="title">Mechanisation of AKS Algorithm: Part 1 – the Main Theorem</span></div><div class="paper"><span class="authors"><span>Mariano Moscato, <a href="http://shemesh.larc.nasa.gov/people/cam">Cesar Munoz</a> and Andrew Smith</span>. </span><span class="title">Affine Arithmetic and Applications to Real-Number Proving</span></div><div class="paper"><span class="authors"><span><a href="http://www.thomas-tuerk.de/en">Thomas Tuerk</a>, <a href="http://www.cl.cam.ac.uk/~mom22">Magnus O. Myreen</a> and <a href="http://www.cl.cam.ac.uk/~rk436">Ramana Kumar</a></span>. </span><span class="title">Pattern Matches in HOL: A New Representation and Improved Code Generation</span></div><div class="paper"><span class="authors"><span>Frédéric Besson, <a href="http://www.irisa.fr/celtique/blazy">Sandrine Blazy</a> and Pierre Wilke</span>. </span><span class="title">A Concrete Memory Model for CompCert</span></div><div class="paper"><span class="authors"><span><a href="https://www.ps.uni-saarland.de/~sdschn">Sigurd Schneider</a>, <a href="https://www.ps.uni-saarland.de/~smolka/">Gert Smolka</a> and <a href="http://compilers.cs.uni-saarland.de/people/hack/">Sebastian Hack</a></span>. </span><span class="title">A First-Order Functional Intermediate Language for Verified Compilers</span></div><div class="paper"><span class="authors"><span>Benja Fallenstein and <a href="http://www.cl.cam.ac.uk/~rk436/">Ramana Kumar</a></span>. </span><span class="title">Proof-Producing Reflection for HOL, with an Application to Model Polymorphism</span></div><div class="paper"><span class="authors">Peter Lammich. </span><span class="title">Refinement to Imperative/HOL</span></div><div class="paper"><span class="authors"><span>Mohammad Abdulaziz, <a href="http://nicta.com.au/people/norrishm">Michael Norrish</a> and <a href="http://users.cecs.anu.edu.au/~charlesg/">Charles Gretton</a></span>. </span><span class="title">Verified, Practical Upper Bounds for State Space Diameters</span></div><div class="paper"><span class="authors"><span><a href="http://www.risec.aist.go.jp/">Reynald Affeldt</a> and <a href="http://www.math.nagoya-u.ac.jp/~garrigue/">Jacques Garrigue</a></span>. </span><span class="title">Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory</span></div><div class="paper"><span class="authors"><span><a href="http://cs.au.dk/~filips">Filip Sieczkowski</a>, <a href="http://cs.au.dk/~abizjak">Aleš Bizjak</a> and <a href="http://www.cs.au.dk/~birke">Lars Birkedal</a></span>. </span><span class="title">ModuRes: a Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming Languages</span></div><div class="paper"><span class="authors">Prathamesh T. </span><span class="title">Formalizing Knot Theory in Isabelle/HOL</span></div><div class="paper"><span class="authors"><span><a href="http://cl-informatik.uibk.ac.at/~griff/">Christian Sternagel</a> and <a href="http://cl-informatik.uibk.ac.at/~thiemann/">René Thiemann</a></span>. </span><span class="title">Deriving Comparators and Show-Functions in Isabelle/HOL</span></div><div class="paper"><span class="authors"><span><a href="http://cl-informatik.uibk.ac.at/users/cek/">Cezary Kaliszyk</a>, <a href="http://cs.ru.nl/~urban/">Josef Urban</a> and Jiri Vyskocil</span>. </span><span class="title">Learning To Parse on Aligned Corpora (Rough Diamond)</span></div><div class="paper"><span class="authors"><span><a href="http://www.cs.cornell.edu/~aa755/">Abhishek Anand</a> and <a href="http://www.cs.cornell.edu/~rak/">Ross Knepper</a></span>. </span><span class="title">ROSCoq: Robots powered by Constructive Reals</span></div><div class="paper"><span class="authors"><span><a href="http://ps.uni-saarland.de/~smolka">Gert Smolka</a>, <a href="http://www.ps.uni-saarland.de/~schaefer">Steven Schäfer</a> and <a href="http://www.ps.uni-saarland.de/~doczkal">Christian Doczkal</a></span>. </span><span class="title">Transfinite Constructions in Classical Type Theory</span></div><div class="paper"><span class="authors">Fabian Immler. </span><span class="title">A Verified Enclosure for the Lorenz Attractor (Rough Diamond)</span></div><div class="paper"><span class="authors"><span>Steven Schäfer, Tobias Tebbi and <a href="http://ps.uni-sb.de/~smolka">Gert Smolka</a></span>. </span><span class="title">Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions</span></div><div class="paper"><span class="authors"><span><a href="https://zoep.github.io/">Zoe Paraskevopoulou</a>, <a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Catalin Hritcu</a>, <a href="http://www.maximedenes.fr">Maxime Dénès</a>, <a href="http://www.cis.upenn.edu/~llamp/">Leonidas Lampropoulos</a> and <a href="http://www.cis.upenn.edu/~bcpierce">Benjamin Pierce</a></span>. </span><span class="title">Foundational Property-Based Testing</span></div><div class="paper"><span class="authors">Régis Spadotti. </span><span class="title">A Mechanized Theory of regular trees in dependent type theory</span></div><div class="paper"><span class="authors"><span>Ondřej Kunčar and Andrei Popescu</span>. </span><span class="title">A Consistent Foundation for Isabelle/HOL</span></div><div class="paper"><span class="authors"><span><a href="http://www.irisa.fr/celtique/blazy">Sandrine Blazy</a>, <a href="http://www.irisa.fr/celtique/demange/">Delphine Demange</a> and <a href="http://www.irisa.fr/celtique/pichardie/">David Pichardie</a></span>. </span><span class="title">Validating Dominator Trees for a Fast, Verified Dominance Test</span></div></body>
+</html>
--- a/bids-2016.html	Mon May 18 16:16:31 2015 +0100
+++ b/bids-2016.html	Mon May 18 16:25:51 2015 +0100
@@ -94,6 +94,7 @@
 [<A HREF="index.html">Home</A>]
 [<A HREF="index.html#dates">Important Dates</A>]
 [<A HREF="cfp.pdf">CFP</A>]
+[<A HREF="accepted.html">Accepted Papers</A>]
 [<A HREF="index.html#committees">Committees</A>]
 [<A HREF="history.html">Conference History</A>]
 <HR>
--- a/history.html	Mon May 18 16:16:31 2015 +0100
+++ b/history.html	Mon May 18 16:25:51 2015 +0100
@@ -93,6 +93,7 @@
 [<A HREF="index.html">Home</A>]
 [<A HREF="index.html#dates">Important Dates</A>]
 [<A HREF="cfp.pdf">CFP</A>]
+[<A HREF="accepted.html">Accepted Papers</A>]
 [<A HREF="index.html#committees">Committees</A>]
 [<A HREF="bids-2016.html">ITP 2016 Bids</A>]
 <HR>
--- a/index.html	Mon May 18 16:16:31 2015 +0100
+++ b/index.html	Mon May 18 16:25:51 2015 +0100
@@ -117,6 +117,7 @@
 [<A HREF="index.html#dates">Important Dates</A>]
 [<A HREF="cfp.pdf">CFP</A>]
 [<A HREF="index.html#committees">Committees</A>]
+[<A HREF="accepted.html">Accepted Papers</A>]
 [<A HREF="history.html">Conference History</A>]
 [<A HREF="bids-2016.html">ITP 2016 Bids</A>]
 <HR>
itp-2015