Abstract is missing.
- π n (S n ) in Homotopy Type TheoryDaniel R. Licata, Guillaume Brunerie. 1-16 [doi]
- Mostly Sound Type System Improves a Foundational Program VerifierJosiah Dodds, Andrew W. Appel. 17-32 [doi]
- Computational Verification of Network Programs in CoqGordon Stewart. 33-49 [doi]
- Aliasing Restrictions of C11 Formalized in CoqRobbert Krebbers. 50-65 [doi]
- Proof Pearl: A Verified Bignum Implementation in x86-64 Machine CodeMagnus O. Myreen, Gregorio Curello. 66-81 [doi]
- A Constructive Theory of Regular Languages in CoqChristian Doczkal, Jan-Oliver Kaiser, Gert Smolka. 82-97 [doi]
- Certified Parsing of Regular LanguagesDenis Firsov, Tarmo Uustalu. 98-113 [doi]
- Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted MetatheoryAndreas Schropp, Andrei Popescu 0001. 114-130 [doi]
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOLBrian Huffman, Ondrej Kuncar. 131-146 [doi]
- Refinements for Free!Cyril Cohen, Maxime Dénès, Anders Mörtberg. 147-162 [doi]
- A Formal Proof of Borodin-Trakhtenbrot's Gap TheoremAndrea Asperti. 163-177 [doi]
- Certified Kruskal's Tree TheoremChristian Sternagel. 178-193 [doi]
- Extracting Proofs from Tabled Proof SearchDale Miller, Alwen Tiu. 194-210 [doi]
- Formalizing the SAFECode Type SystemDaniel Huang, Greg Morrisett. 211-226 [doi]
- Certifiably Sound Parallelizing TransformationsChristian J. Bell. 227-242 [doi]
- Programming Type-Safe Transformations Using Higher-Order Abstract SyntaxOlivier Savary Belanger, Stefan Monnier, Brigitte Pientka. 243-258 [doi]
- Formalizing Probabilistic NoninterferenceAndrei Popescu 0001, Johannes Hölzl, Tobias Nipkow. 259-275 [doi]
- Machine Assisted Proof of ARMv7 Instruction Level Isolation PropertiesNarges Khakpour, Oliver Schwarz, Mads Dam. 276-291 [doi]
- A Formal Model and Correctness Proof for an Access Control Policy FrameworkChunhan Wu, Xingyuan Zhang, Christian Urban. 292-307 [doi]