Abstract is missing.
- POPLMark reloaded: mechanizing logical relations proofs (invited talk)Brigitte Pientka. 1 [doi]
- Efficient certification of complexity proofs: formalizing the Perron-Frobenius theorem (invited talk paper)Jose Divasón, Sebastiaan J. C. Joosten, Ondrej Kuncar, René Thiemann, Akihisa Yamada 0002. 2-13 [doi]
- Total Haskell is reasonable CoqAntal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich. 14-27 [doi]
- A formal proof in Coq of a control function for the inverted pendulumDamien Rouhling. 28-41 [doi]
- Completeness and decidability of converse PDL in the constructive type theory of CoqChristian Doczkal, Joachim Bard. 42-52 [doi]
- Mechanising and verifying the WebAssembly specificationConrad Watt. 53-65 [doi]
- Towards verifying ethereum smart contract bytecode in Isabelle/HOLSidney Amani, Myriam Bégel, Maksym Bortin, Mark Staples. 66-77 [doi]
- Mechanising blockchain consensusGeorge Pîrlea, Ilya Sergey. 78-90 [doi]
- Formal microeconomic foundations and the first welfare theoremCezary Kaliszyk, Julian Parsert. 91-101 [doi]
- Triangulating context lemmasCraig McLaughlin, James McKinna, Ian Stark. 102-114 [doi]
- Adapting proof automation to adapt proofsTalia Ringer, Nathaniel Yazdani, John Leo, Dan Grossman. 115-129 [doi]
- A monadic framework for relational verification: applied to information security, program equivalence, and optimizationsNiklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella Béguelin. 130-145 [doi]
- Formal proof of polynomial-time complexity with quasi-interpretationsHugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak. 146-157 [doi]
- A verified SAT solver with watched literals using imperative HOLMathias Fleury, Jasmin Christian Blanchette, Peter Lammich. 158-171 [doi]
- Œuf: minimizing the Coq extraction TCBEric Mullen, Stuart Pernsteiner, James R. Wilcox, Zachary Tatlock, Dan Grossman. 172-185 [doi]
- Proofs in conflict-driven theory combinationMaria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar. 186-200 [doi]
- Finite sets in homotopy type theoryDan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide. 201-214 [doi]
- Generic derivation of induction for impredicative encodings in CedilleDenis Firsov, Aaron Stump. 215-227 [doi]
- Large model constructions for second-order ZF in dependent type theoryDominik Kirst, Gert Smolka. 228-239 [doi]
- A constructive formalisation of Semi-algebraic sets and functionsBoris Djalal. 240-251 [doi]
- HOπ in CoqSergueï Lenglet, Alan Schmitt. 252-265 [doi]
- A Coq formalization of normalization by evaluation for Martin-Löf type theoryPawel Wieczorek, Dariusz Biernacki. 266-279 [doi]
- A two-level logic perspective on (simultaneous) substitutionsKaustuv Chaudhuri. 280-292 [doi]
- Binder aware recursion over well-scoped de Bruijn syntaxJonas Kaiser, Steven Schäfer, Kathrin Stark. 293-306 [doi]