Abstract is missing.
- Perspectives on formal verification (invited talk)Harvey M. Friedman. 1 [doi]
- Dependent type practice (invited talk)Leonardo Mendonça de Moura. 2 [doi]
- Higher-order representation predicates in separation logicArthur Charguéraud. 3-14 [doi]
- A unified Coq framework for verifying C programs with floating-point computationsTahina Ramananandro, Paul Mountcastle, Benoît Meister, Richard Lethin. 15-26 [doi]
- Refinement based verification of imperative data structuresPeter Lammich. 27-36 [doi]
- The vampire and the FOOLEvgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov. 37-48 [doi]
- Improving automation in interactive theorem provers by efficient encoding of lambda-abstractionsLukasz Czajka 0001. 49-57 [doi]
- Towards a mizar environment for isabelle: foundations and languageCezary Kaliszyk, Karol Pak, Josef Urban. 58-65 [doi]
- A modular, efficient formalisation of real algebraic numbersWenda Li, Lawrence C. Paulson. 66-75 [doi]
- Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomialsSophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub. 76-87 [doi]
- Formalizing jordan normal forms in Isabelle/HOLRené Thiemann, Akihisa Yamada 0002. 88-99 [doi]
- Formalization of a newton series representation of polynomialsCyril Cohen, Boris Djalal. 100-109 [doi]
- A logic of proofs for differential dynamic logic: toward independently checkable proof certificates for dynamic logicsNathan Fulton, André Platzer. 110-121 [doi]
- Constructing the propositional truncation using non-recursive HITsFloris van Doorn. 122-129 [doi]
- A nominal exploration of intuitionismVincent Rahli, Mark Bickford. 130-141 [doi]
- Bisimulation up-to techniques for psi-calculiJohannes Åman Pohjola, Joachim Parrow. 142-153 [doi]
- Planning for change in a formal verification of the raft consensus protocolDoug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, Thomas E. Anderson. 154-165 [doi]
- A verified algorithm for detecting conflicts in XACML access control rulesMichel St-Martin, Amy P. Felty. 166-175 [doi]
- Formal verification of control-flow graph flatteningSandrine Blazy, Alix Trieu. 176-187 [doi]
- Axiomatic semantics for compiler verificationSteven Schäfer, Sigurd Schneider, Gert Smolka. 188-196 [doi]