Abstract is missing.
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional AnalysisReynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi. 3-20 [doi]
- A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper)Anne Baanen. 21-27 [doi]
- Practical Proof Search for Coq by Type InhabitationLukasz Czajka 0001. 28-57 [doi]
- Quotients of Bounded Natural FunctorsBasil Fürer, Andreas Lochbihler, Joshua Schneider 0001, Dmitriy Traytel. 58-78 [doi]
- Trakhtenbrot's Theorem in Coq - A Constructive Approach to Finite Model TheoryDominik Kirst, Dominique Larchey-Wendling. 79-96 [doi]
- Deep Generation of Coq Lemma Names Using Elaborated TermsPengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric. 97-118 [doi]
- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and ProofsClément Pit-Claudel, Peng Wang 0048, Benjamin Delaware, Jason Gross, Adam Chlipala. 119-137 [doi]
- Validating Mathematical StructuresKazuhiko Sakaguchi. 138-157 [doi]
- Teaching Automated Theorem Proving by Example: PyRes 1.2 - (System Description)Stephan Schulz 0001, Adam Pease. 158-166 [doi]
- Beyond Notations: Hygienic Macro Expansion for Theorem Proving LanguagesSebastian Ullrich, Leonardo de Moura. 167-182 [doi]
- Formalizing the Face Lattice of PolyhedraXavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub. 185-203 [doi]
- Algebraically Closed Fields in Isabelle/HOLPaulo Emílio de Vilhena, Lawrence C. Paulson. 204-220 [doi]
- Formalization of Forcing in Isabelle/ZFEmmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf. 221-235 [doi]
- Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOLWalter Guttmann. 236-253 [doi]
- Formal Proof of the Group Law for Edwards Elliptic CurvesThomas C. Hales, Rodrigo Raya. 254-269 [doi]
- Verifying Faradžev-Read Type Isomorph-Free Exhaustive GenerationFilip Maric. 270-287 [doi]
- Verified Approximation AlgorithmsRobin Eßmann, Tobias Nipkow, Simon Robillard. 291-306 [doi]
- Efficient Verified Implementation of Introsort and PdqsortPeter Lammich. 307-323 [doi]
- A Fast Verified Liveness Analysis in SSA FormJean-Christophe Léchenet, Sandrine Blazy, David Pichardie. 324-340 [doi]
- Verification of Closest Pair of Points AlgorithmsMartin Rau, Tobias Nipkow. 341-357 [doi]
- A Polymorphic Vampire - (Short Paper)Ahmed Bhayat, Giles Reger. 361-368 [doi]
- N-PAT: A Nested Model-Checker - (System Description)Hadrien Bride, Cheng-Hao Cai, Jin Song Dong, Rajeev Goré, Zhé Hóu, Brendan P. Mahony, Jim McCarthy. 369-377 [doi]
- HYPNO: Theorem Proving with Hypersequent Calculi for Non-normal Modal Logics (System Description)Tiziano Dalmonte, Nicola Olivetti, Gian Luca Pozzato. 378-387 [doi]
- Implementing Superposition in iProver (System Description)André Duarte, Konstantin Korovin. 388-397 [doi]
- MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)Marianna Girlando, Lutz Straßburger. 398-407 [doi]
- Make E Smart Again (Short Paper)Zarathustra Amadeus Goertzel. 408-415 [doi]
- Automatically Proving and Disproving Feasibility ConditionsRaúl Gutiérrez, Salvador Lucas. 416-435 [doi]
- mu-term: Verify Termination Properties Automatically (System Description)Raúl Gutiérrez, Salvador Lucas. 436-447 [doi]
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda 0001, Josef Urban. 448-463 [doi]
- The Imandra Automated Reasoning System (System Description)Grant O. Passmore, Simon Cruanes, Denis Ignatovich, Dave Aitken, Matt Bray, Elijah Kagan, Kostya Kanishev, Ewen Maclean, Nicola Mometto. 464-471 [doi]
- A Programmer's Text Editor for a Logical Theory: The SUMOjEdit Editor (System Description)Adam Pease. 472-479 [doi]
- Sequoia: A Playground for Logicians - (System Description)Giselle Reis, Zan Naeem, Mohammed Hashim. 480-488 [doi]
- Prolog Technology Reinforcement Learning Prover - (System Description)Zsolt Zombori, Josef Urban, Chad E. Brown. 489-507 [doi]