Abstract is missing.
- Verified Over-Approximation of the Diameter of Propositionally Factored Transition SystemsMohammad Abdulaziz, Charles Gretton, Michael Norrish. 1-16 [doi]
- Formalization of Error-Correcting Codes: From Hamming to Modern Coding TheoryReynald Affeldt, Jacques Garrigue. 17-33 [doi]
- ROSCoq: Robots Powered by Constructive RealsAbhishek Anand, Ross A. Knepper. 34-50 [doi]
- Asynchronous Processing of Coq Documents: From the Kernel up to the User InterfaceBruno Barras, Carst Tankink, Enrico Tassi. 51-66 [doi]
- A Concrete Memory Model for CompCertFrédéric Besson, Sandrine Blazy, Pierre Wilke. 67-83 [doi]
- Validating Dominator Trees for a Fast, Verified Dominance TestSandrine Blazy, Delphine Demange, David Pichardie. 84-99 [doi]
- Refinement to Certify Abstract Interpretations, Illustrated on Linearization for PolyhedraSylvain Boulmé, Alexandre Maréchal. 100-116 [doi]
- Mechanisation of AKS Algorithm: Part 1 - The Main TheoremHing-Lun Chan, Michael Norrish. 117-136 [doi]
- Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find ImplementationArthur Charguéraud, François Pottier. 137-153 [doi]
- Formalizing Size-Optimal Sorting Networks: Extracting a Certified Proof CheckerLuís Cruz-Filipe, Peter Schneider-Kamp. 154-169 [doi]
- Proof-Producing Reflection for HOL - With an Application to Model PolymorphismBenja Fallenstein, Ramana Kumar. 170-186 [doi]
- Improved Tool Support for Machine-Code Decompilation in HOL4Anthony C. J. Fox. 187-202 [doi]
- A Formalized Hierarchy of Probabilistic System Types - Proof PearlJohannes Hölzl, Andreas Lochbihler, Dmitriy Traytel. 203-220 [doi]
- A Verified Enclosure for the Lorenz Attractor (Rough Diamond)Fabian Immler. 221-226 [doi]
- Learning to Parse on Aligned Corpora (Rough Diamond)Cezary Kaliszyk, Josef Urban, Jirí Vyskocil. 227-233 [doi]
- A Consistent Foundation for Isabelle/HOLOndrej Kuncar, Andrei Popescu 0001. 234-252 [doi]
- Refinement to Imperative/HOLPeter Lammich. 253-269 [doi]
- Stream Fusion for Isabelle's Code Generator - Rough DiamondAndreas Lochbihler, Alexandra Maximova. 270-277 [doi]
- HOCore in CoqPetar Maksimovic, Alan Schmitt. 278-293 [doi]
- Affine Arithmetic and Applications to Real-Number ProvingMariano M. Moscato, César A. Muñoz, Andrew P. Smith. 294-309 [doi]
- Amortized Complexity VerifiedTobias Nipkow. 310-324 [doi]
- Foundational Property-Based TestingZoe Paraskevopoulou, Catalin Hritcu, Maxime Dénès, Leonidas Lampropoulos, Benjamin C. Pierce. 325-343 [doi]
- A Linear First-Order Functional Intermediate Language for Verified CompilersSigurd Schneider, Gert Smolka, Sebastian Hack. 344-358 [doi]
- Autosubst: Reasoning with de Bruijn Terms and Parallel SubstitutionsSteven Schäfer, Tobias Tebbi, Gert Smolka. 359-374 [doi]
- ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming LanguagesFilip Sieczkowski, Ales Bizjak, Lars Birkedal. 375-390 [doi]
- Transfinite Constructions in Classical Type TheoryGert Smolka, Steven Schäfer, Christian Doczkal. 391-404 [doi]
- A Mechanized Theory of Regular Trees in Dependent Type TheoryRégis Spadotti. 405-420 [doi]
- Deriving Comparators and Show Functions in Isabelle/HOLChristian Sternagel, René Thiemann. 421-437 [doi]
- Formalising Knot Theory in Isabelle/HOLT. V. H. Prathamesh. 438-452 [doi]
- Pattern Matches in HOL: - A New Representation and Improved Code GenerationThomas Tuerk, Magnus O. Myreen, Ramana Kumar. 453-468 [doi]