Abstract is missing.
- An Isabelle/HOL Formalisation of Green's TheoremMohammad Abdulaziz, Lawrence C. Paulson. 3-19 [doi]
- HOL Zero's Solutions for Pollack-InconsistencyMark Adams. 20-35 [doi]
- Infeasible Paths Elimination by Symbolic Execution Techniques - Proof of Correctness and Preservation of PathsRomain Aissat, Frédéric Voisin, Burkhart Wolff. 36-51 [doi]
- Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced ConcurrencyJune Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan, Christine Rizkallah. 52-68 [doi]
- POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)Fahad Ausaf, Roy Dyckhoff, Christian Urban. 69-86 [doi]
- CoSMed: A Confidentiality-Verified Social Media PlatformThomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu 0001, Franco Raimondi. 87-106 [doi]
- Mechanical Verification of a Constructive Proof for FLPBenjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters, Uwe Nestmann. 107-122 [doi]
- Visual Theorem Proving with the Incredible Proof MachineJoachim Breitner. 123-139 [doi]
- Proof Pearl: Bounding Least Common Multiples with TrianglesHing-Lun Chan, Michael Norrish. 140-150 [doi]
- Two-Way Automata in CoqChristian Doczkal, Gert Smolka. 151-166 [doi]
- Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil AlgorithmsThomas Grégoire, Adam Chlipala. 167-183 [doi]
- The Flow of ODEsFabian Immler, Christoph Traut. 184-199 [doi]
- From Types to Sets by Local Type Definitions in Higher-Order LogicOndrej Kuncar, Andrei Popescu 0001. 200-218 [doi]
- Formalizing the Edmonds-Karp AlgorithmPeter Lammich, S. Reza Sefidgar. 219-234 [doi]
- A Formal Proof of Cauchy's Residue TheoremWenda Li, Lawrence C. Paulson. 235-251 [doi]
- Equational Reasoning with Applicative FunctorsAndreas Lochbihler, Joshua Schneider. 252-273 [doi]
- Formally Verified Approximations of Definite IntegralsAssia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote. 274-289 [doi]
- Certification of Classical Confluence Results for Left-Linear Term Rewrite SystemsJulian Nagele, Aart Middeldorp. 290-306 [doi]
- Automatic Functional Correctness Proofs for Functional Search TreesTobias Nipkow. 307-322 [doi]
- A Framework for the Automatic Formal Verification of Refinement from Cogent to CChristine Rizkallah, Japheth Lim, Yutaka Nagashima, Thomas Sewell, Zilin Chen, Liam O'Connor, Toby C. Murray, Gabriele Keller, Gerwin Klein. 323-340 [doi]
- Formalization of the Resolution Calculus for First-Order LogicAnders Schlichtkrull. 341-357 [doi]
- Verified Operational Transformation for TreesSergey Sinchuk, Pavel Chuprikov, Konstantin Solomatov. 358-373 [doi]
- Hereditarily Finite Sets in Constructive Type TheoryGert Smolka, Kathrin Stark. 374-390 [doi]
- Algebraic Numbers in Isabelle/HOLRené Thiemann, Akihisa Yamada 0002. 391-408 [doi]
- Modular Dependent Induction in Coq, Mendler-StylePaolo Torrini. 409-424 [doi]
- Formalized Timed AutomataSimon Wimmer. 425-440 [doi]
- AUTO2, A Saturation-Based Heuristic Prover for Higher-Order LogicBohua Zhan. 441-456 [doi]
- What's in a Theorem Name?David Aspinall 0001, Cezary Kaliszyk. 459-465 [doi]
- Cardinalities of Finite Relations in CoqPaul Brunet, Damien Pous, Insa Stucke. 466-474 [doi]
- Formalising Semantics for Expected Running Time of Probabilistic ProgramsJohannes Hölzl. 475-482 [doi]
- On the Formalization of Fourier Transform in Higher-order LogicAdnan Rashid, Osman Hasan. 483-490 [doi]
- CoqPIE: An IDE Aimed at Improving Proof Development Productivity - (Rough Diamond)Kenneth Roe, Scott Smith. 491-499 [doi]