Mercurial Mercurial > hg > itp-2015 / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
accepted.html
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Thu, 27 Aug 2015 09:03:41 +0800
changeset 330 9351eb58caa1
parent 196 2772f5f48524
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
131
a5c905a33751 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     1
 
<!DOCTYPE html
a5c905a33751 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     2
 
      PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
a5c905a33751 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     3
 
      "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
a5c905a33751 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     4
 
<html lang="en-US" xmlns="http://www.w3.org/1999/xhtml" xml:lang="en-US" style="display:none">
a5c905a33751 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     5
 
<head>
a5c905a33751 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     6
 
<title>ITP 2015 Accepted Papers</title>
a5c905a33751 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     7
 
<script>window['ec:pageId']='11624752626377228288'</script>
a5c905a33751 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     8
 
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
a5c905a33751 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
     9
 
<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>
196
2772f5f48524 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 131
diff changeset 
    10
 
<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 Over-Approximation of the Diameters of Propositionally Factored Transition Systems</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>
131
a5c905a33751 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset 
    11
 
</html>
itp-2015