diff -r e3712a3835a0 -r 2772f5f48524 accepted.html --- a/accepted.html Sat Jun 20 08:19:12 2015 +0800 +++ b/accepted.html Sun Jun 21 20:47:36 2015 +0100 @@ -7,5 +7,5 @@ -

ITP 2015 Accepted Papers

Andreas Lochbihler and Alexandra Maximova. Stream Fusion for Isabelle’s Code Generator (Rough Diamond)

Luís Cruz-Filipe and Peter Schneider-Kamp. Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof Checker

Bruno Barras, Carst Tankink and Enrico Tassi. Asynchronous processing of Coq documents: from the kernel up to the user interface

Tobias Nipkow. Amortized Complexity Verified

Anthony Fox. Improved Tool Support for Machine-Code Decompilation in HOL4

Sylvain Boulmé and Alexandre Maréchal. Refinement to certify abstract interpretations, illustrated on linearization for polyhedra.

Arthur Charguéraud and François Pottier. Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation

Johannes Hölzl, Andreas Lochbihler and Dmitriy Traytel. A Formalized Hierarchy of Probabilistic System Types (Proof Pearl)

Petar Maksimovic and Alan Schmitt. HOCore in Coq

Hing-Lun Chan and Michael Norrish. Mechanisation of AKS Algorithm: Part 1 – the Main Theorem

Mariano Moscato, Cesar Munoz and Andrew Smith. Affine Arithmetic and Applications to Real-Number Proving

Thomas Tuerk, Magnus O. Myreen and Ramana Kumar. Pattern Matches in HOL: A New Representation and Improved Code Generation

Frédéric Besson, Sandrine Blazy and Pierre Wilke. A Concrete Memory Model for CompCert

Sigurd Schneider, Gert Smolka and Sebastian Hack. A First-Order Functional Intermediate Language for Verified Compilers

Benja Fallenstein and Ramana Kumar. Proof-Producing Reflection for HOL, with an Application to Model Polymorphism

Peter Lammich. Refinement to Imperative/HOL

Mohammad Abdulaziz, Michael Norrish and Charles Gretton. Verified, Practical Upper Bounds for State Space Diameters

Reynald Affeldt and Jacques Garrigue. Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory

Filip Sieczkowski, Aleš Bizjak and Lars Birkedal. ModuRes: a Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming Languages

Prathamesh T. Formalizing Knot Theory in Isabelle/HOL

Christian Sternagel and René Thiemann. Deriving Comparators and Show-Functions in Isabelle/HOL

Cezary Kaliszyk, Josef Urban and Jiri Vyskocil. Learning To Parse on Aligned Corpora (Rough Diamond)

Abhishek Anand and Ross Knepper. ROSCoq: Robots powered by Constructive Reals

Gert Smolka, Steven Schäfer and Christian Doczkal. Transfinite Constructions in Classical Type Theory

Fabian Immler. A Verified Enclosure for the Lorenz Attractor (Rough Diamond)

Steven Schäfer, Tobias Tebbi and Gert Smolka. Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions

Zoe Paraskevopoulou, Catalin Hritcu, Maxime Dénès, Leonidas Lampropoulos and Benjamin Pierce. Foundational Property-Based Testing

Régis Spadotti. A Mechanized Theory of regular trees in dependent type theory

Ondřej Kunčar and Andrei Popescu. A Consistent Foundation for Isabelle/HOL

Sandrine Blazy, Delphine Demange and David Pichardie. Validating Dominator Trees for a Fast, Verified Dominance Test