Abstract is missing.
- Matching logic: the foundation of the K framework (invited talk)Grigore Rosu, Xiaohong Chen 0002. 1 [doi]
- Proof assistants at the hardware-software interface (invited talk)Adam Chlipala. 2 [doi]
- A verified packrat parser interpreter for parsing expression grammarsClement Blaudeau, Natarajan Shankar. 3-17 [doi]
- Proof pearl: Braun treesTobias Nipkow, Thomas Sewell. 18-31 [doi]
- FreeSpec: specifying, verifying, and executing impure computations in CoqThomas Letan, Yann Régis-Gianas. 32-46 [doi]
- Verifying x86 instruction implementationsShilpi Goel, Anna Slobodová, Rob Sumners, Sol Swords. 47-60 [doi]
- Frying the egg, roasting the chicken: unit deletions in DRAT proofsJohannes Altmanninger, Adrián Rebola-Pardo. 61-70 [doi]
- An equational theory for weak bisimulation via generalized parameterized coinductionYannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic. 71-84 [doi]
- Exploration of neural machine translation in autoformalization of mathematics in MizarQingxiang Wang, Chad E. Brown, Cezary Kaliszyk, Josef Urban. 85-98 [doi]
- REPLica: REPL instrumentation for Coq analysisTalia Ringer, Alex Sanchez-Stern, Dan Grossman, Sorin Lerner. 99-113 [doi]
- Verified programming of Turing machines in CoqYannick Forster 0002, Fabian Kunze, Maximilian Wuttke. 114-128 [doi]
- A functional proof pearl: inverting the Ackermann hierarchyLinh Tran, Anshuman Mohan, Aquinas Hobor. 129-142 [doi]
- Undecidability of higher-order unification formalised in CoqSimon Spies, Yannick Forster 0002. 143-157 [doi]
- Cubical synthetic homotopy theoryAnders Mörtberg, Loïc Pujet. 158-171 [doi]
- Three equivalent ordinal notation systems in cubical AgdaFredrik Nordvall Forsberg, Chuangjie Xu, Neil Ghani. 172-185 [doi]
- Coq à la carte: a practical approach to modular syntax with bindersYannick Forster 0002, Kathrin Stark. 186-200 [doi]
- A mechanized formalization of GraphQLTomás Díaz, Federico Olmedo, Éric Tanter. 201-214 [doi]
- ConCert: a smart contract certification framework in CoqDanil Annenkov, Jakob Botsch Nielsen, Bas Spitters. 215-228 [doi]
- Formalising oblivious transfer in the semi-honest and malicious model in CryptHOLDavid Butler 0002, David Aspinall 0001, Adrià Gascón. 229-243 [doi]
- Verified security of BLT signature schemeDenis Firsov, Ahto Buldas, Ahto Truu, Risto Laanoja. 244-257 [doi]
- Formalizing determinacy of concurrent revisionsRoy Overbeek. 258-269 [doi]
- Formalizing π-calculus in guarded cubical AgdaNiccolò Veltri, Andrea Vezzosi. 270-283 [doi]
- Intrinsically-typed definitional interpreters for linear, session-typed languagesArjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser. 284-298 [doi]
- Formalising perfectoid spacesKevin Buzzard, Johan Commelin, Patrick Massot. 299-312 [doi]
- A constructive formalization of the weak perfect graph theoremAbhishek Kr Singh, Raja Natarajan. 313-324 [doi]
- Completeness of an axiomatization of graph isomorphism via graph rewriting in CoqChristian Doczkal, Damien Pous. 325-337 [doi]
- The Poincaré-Bendixson theorem in Isabelle/HOLFabian Immler, Yong Kiam Tan. 338-352 [doi]
- A formal proof of the independence of the continuum hypothesisJesse Michael Han, Floris van Doorn. 353-366 [doi]
- The lean mathematical library367-381 [doi]