Abstract is missing.
- Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)Jasmin Christian Blanchette. 1-13 [doi]
- A linear logical framework in hybrid (invited talk)Amy P. Felty. 14 [doi]
- A formal proof of hensel's lemma over the p-adic integersRobert Y. Lewis. 15-26 [doi]
- Verified solving and asymptotics of linear recurrencesManuel Eberl. 27-37 [doi]
- On synthetic undecidability in coq, with an application to the entscheidungsproblemYannick Forster 0002, Dominik Kirst, Gert Smolka. 38-51 [doi]
- Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theoremWenda Li, Lawrence C. Paulson. 52-64 [doi]
- Smooth manifolds and types to sets for linear algebra in Isabelle/HOLFabian Immler, Bohua Zhan. 65-77 [doi]
- A proof-theoretic approach to certifying skolemizationKaustuv Chaudhuri, Matteo Manighetti, Dale Miller 0001. 78-90 [doi]
- Eliminating reflection from type theoryThéo Winterhalter, Matthieu Sozeau, Nicolas Tabareau. 91-103 [doi]
- Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machinesYannick Forster, Dominique Larchey-Wendling. 104-117 [doi]
- Call-by-push-value in coq: operational, equational, and denotational theoryYannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark. 118-131 [doi]
- A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOLBertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, Franziska Rapp. 132-143 [doi]
- Certified ACKBOAlexander Lochmann, Christian Sternagel. 144-151 [doi]
- A verified prover based on ordered resolutionAnders Schlichtkrull, Jasmin Christian Blanchette, Dmitriy Traytel. 152-165 [doi]
- Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutionsKathrin Stark, Steven Schäfer, Jonas Kaiser. 166-180 [doi]
- Formally verified big step semantics out of x86-64 binariesIan Roessle, Freek Verbeek, Binoy Ravindran. 181-195 [doi]
- Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressionsSandrine Blazy, Rémi Hutin. 196-208 [doi]
- Dynamic class initialization semantics: a jinja extensionSusannah Mansky, Elsa L. Gunter. 209-221 [doi]
- A verified protocol buffer compilerQianchuan Ye, Benjamin Delaware. 222-233 [doi]
- From C to interaction trees: specifying, verifying, and testing a networked serverNicolas Koh, Yao Li 0004, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, Steve Zdancewic. 234-248 [doi]
- A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebraVéronique Benzaken, Evelyne Contejean. 249-261 [doi]