Abstract is missing.
- Automated Theory Exploration for Interactive Theorem Proving: - An Introduction to the Hipster SystemMoa Johansson. 1-11 [doi]
- Automating Formalization by Statistical and Semantic Parsing of MathematicsCezary Kaliszyk, Josef Urban, Jirí Vyskocil. 12-27 [doi]
- A Formalization of Convex Polyhedra Based on the Simplex MethodXavier Allamigeon, Ricardo D. Katz. 28-45 [doi]
- A Formal Proof of the Expressiveness of Deep LearningAlexander Bentkamp, Jasmin Christian Blanchette, Dietrich Klakow. 46-64 [doi]
- Formalization of the Lindemann-Weierstrass TheoremSophie Bernard. 65-80 [doi]
- CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer SemanticsFrédéric Besson, Sandrine Blazy, Pierre Wilke. 81-97 [doi]
- Formal Verification of a Floating-Point Expansion Renormalization AlgorithmSylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu. 98-113 [doi]
- How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party ComputationDavid Butler, David Aspinall 0001, Adrià Gascón. 114-130 [doi]
- FoCaLiZe and Dedukti to the Rescue for Proof InteroperabilityRaphaël Cauderlier, Catherine Dubois. 131-147 [doi]
- A Formal Proof in Coq of LaSalle's Invariance PrincipleCyril Cohen, Damien Rouhling. 148-163 [doi]
- How to Get More Out of Your OraclesLuís Cruz-Filipe, Kim S. Larsen, Peter Schneider-Kamp. 164-170 [doi]
- Certifying Standard and Stratified Datalog Inference Engines in SSReflectVéronique Benzaken, Evelyne Contejean, Stefania Dumbrava. 171-188 [doi]
- Weak Call-by-Value Lambda Calculus as a Model of Computation in CoqYannick Forster 0002, Gert Smolka. 189-206 [doi]
- Bellerophon: Tactical Theorem Proving for Hybrid SystemsNathan Fulton, Stefan Mitsch, Brandon Bohrer, André Platzer. 207-224 [doi]
- Formalizing Basic Quaternionic AnalysisAndrea Gabrielli, Marco Maggesi. 225-240 [doi]
- A Formalized General Theory of Syntax with BindingsLorenzo Gheri, Andrei Popescu 0001. 241-261 [doi]
- Proof Certificates in PVSFrédéric Gilbert. 262-268 [doi]
- Efficient, Verified Checking of Propositional ProofsMarijn Heule, Warren A. Hunt Jr., Matt Kaufmann, Nathan Wetzler. 269-284 [doi]
- Proof Tactics for Assertions in Separation LogicZhe Hou, David Sanán, Alwen Tiu, Yang Liu. 285-303 [doi]
- Categoricity Results for Second-Order ZF in Dependent Type TheoryDominik Kirst, Gert Smolka. 304-318 [doi]
- Making PVS Accessible to Generic Services by Interpretation in a Universal FormatMichael Kohlhase, Dennis Müller, Sam Owre, Florian Rabe. 319-335 [doi]
- Formally Verified Safe Vertical Maneuvers for Non-deterministic, Accelerating Aircraft DynamicsYanni Kouskoulas, Daniel Genin, Aurora Schmidt, Jean-Baptiste Jeannin. 336-353 [doi]
- Using Abstract Stobjs in ACL2 to Compute Matrix Normal FormsLaureano Lambán, Francisco J. Martín-Mateos, Julio Rubio, José-Luis Ruiz-Reina. 354-370 [doi]
- Typing Total Recursive Functions in CoqDominique Larchey-Wendling. 371-388 [doi]
- Effect Polymorphism in Higher-Order Logic (Proof Pearl)Andreas Lochbihler. 389-409 [doi]
- Schulze Voting as Evidence Carrying ComputationDirk Pattinson, Mukesh Tiwari. 410-426 [doi]
- Verified Spilling and Translation Validation with RepairJulian Rosemann, Sigurd Schneider, Sebastian Hack. 427-443 [doi]
- A Verified Generational Garbage Collector for CakeMLAdam Sandberg Ericsson, Magnus O. Myreen, Johannes Åman Pohjola. 444-461 [doi]
- A Formalisation of Consistent Consequence for Boolean Equation SystemsMyrthe van Delft, Herman Geuvers, Tim A. C. Willemse. 462-478 [doi]
- Homotopy Type Theory in LeanFloris van Doorn, Jakob von Raumer, Ulrik Buchholtz. 479-495 [doi]
- Verifying a Concurrent Garbage Collector Using a Rely-Guarantee MethodologyYannick Zakowski, David Cachera, Delphine Demange, Gustavo Petri, David Pichardie, Suresh Jagannathan, Jan Vitek. 496-513 [doi]
- Formalization of the Fundamental Group in Untyped Set Theory Using Auto2Bohua Zhan. 514-530 [doi]