Abstract is missing.
- Porting the HOL light analysis library: some lessons (invited talk)Lawrence C. Paulson. 1 [doi]
- Mechanized verification of preemptive OS kernels (invited talk)Xinyu Feng. 2 [doi]
- Verifying a hash table and its iterators in higher-order separation logicFrançois Pottier. 3-16 [doi]
- A formalization of the Berlekamp-Zassenhaus factorization algorithmJose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa Yamada 0002. 17-29 [doi]
- Formal foundations of 3D geometry to model robot manipulatorsReynald Affeldt, Cyril Cohen. 30-42 [doi]
- BliStrTune: hierarchical invention of theorem proving strategiesJan Jakubuv, Josef Urban. 43-52 [doi]
- Automatic cyclic termination proofs for recursive procedures in separation logicReuben N. S. Rowe, James Brotherston. 53-65 [doi]
- Formalization of Karp-Miller tree construction on petri netsMitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto. 66-78 [doi]
- A Coq formal proof of the LaxMilgram theoremSylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero. 79-89 [doi]
- A reflexive tactic for polynomial positivity using numerical solvers and floating-point computationsÉrik Martin-Dorel, Pierre Roux. 90-99 [doi]
- Markov processes in Isabelle/HOLJohannes Hölzl. 100-111 [doi]
- Formalising real numbers in homotopy type theoryGaëtan Gilbert. 112-124 [doi]
- Verified compilation of CakeML to multiple machine-code targetsAnthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, Ramana Kumar. 125-137 [doi]
- Complx: a verification framework for concurrent imperative programsSidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, Joseph Tuong. 138-150 [doi]
- Verifying dynamic race detectionWilliam Mansky, Yuanfeng Peng, Steve Zdancewic, Joseph Devietti. 151-163 [doi]
- The HoTT library: a formalization of homotopy type theory in CoqAndrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters. 164-172 [doi]
- Lifting proof-relevant unification to higher dimensionsJesper Cockx, Dominique Devriese. 173-181 [doi]
- The next 700 syntactical models of type theorySimon Boulier, Pierre-Marie Pédrot, Nicolas Tabareau. 182-194 [doi]
- Type-and-scope safe programs and their proofsGuillaume Allais, James Chapman, Conor McBride, James McKinna. 195-207 [doi]
- Formally verified differential dynamic logicBrandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, André Platzer. 208-221 [doi]
- Equivalence of system f and ź2 in Coq based on context morphism lemmasJonas Kaiser, Tobias Tebbi, Gert Smolka. 222-234 [doi]