FLOC 2022: FEDERATED LOGIC CONFERENCE 2022

A
Abrahamsson, Oskar	Candle: A Verified Implementation of HOL Light
B
Baanen, Anne	Use and abuse of instance parameters in the Lean mathematical library
Bapanapally, Jagadish	A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(r)
Becker, Heiko	Dandelion: Certified Approximations of Elementary Functions
Biernacka, Małgorzata	The Zoo of Lambda-Calculus Reduction Strategies, and Coq
Blanchette, Jasmin	Seventeen Provers under the Hammer
C
Charatonik, Witold	The Zoo of Lambda-Calculus Reduction Strategies, and Coq
Chen, Carol	Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
Chlipala, Adam	Accelerating Verified-Compiler Development with a Verified Rewriting Engine Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
D
Darulova, Eva	Dandelion: Certified Approximations of Elementary Functions
de Frutos-Fernández, María Inés	Formalizing the ring of adèles of a global field
Desharnais, Martin	Seventeen Provers under the Hammer
Dillies, Yaël	Formalizing Szemerédi's Regularity Lemma in Lean
Drab, Tomasz	The Zoo of Lambda-Calculus Reduction Strategies, and Coq
Dudenhefner, Andrej	Undecidability of Dyadic First-Order Logic in Coq
Dupuis, Frédéric	Formalized functional analysis with semilinear maps
E
Edmonds, Chelsea	Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics
Erbsen, Andres	Accelerating Verified-Compiler Development with a Verified Rewriting Engine
F
Felty, Amy	(Invited) Modelling and Verifying Properties of Biological Neural Networks
Forster, Yannick	Synthetic Kolmogorov Complexity in Coq
Fox, Anthony	Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification
From, Asta Halkjær	Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
G
Gaboardi, Marco	Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
Gamboa, Ruben	A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(r)
Gengelbach, Arve	A Verified Cyclicity Checker
Goertzel, Zarathustra	The Isabelle ENIGMA
Gross, Jason	Accelerating Verified-Compiler Development with a Verified Rewriting Engine Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
Gómez-Londoño, Alejandro	Kalas: A Verified, End-to-End Compiler for a Choreographic Language
H
Hao, Jifeng	Compositional Verification of Interacting Systems using Event Monads
Hong, Ye	Compositional Verification of Interacting Systems using Event Monads
Hostert, Johannes	Undecidability of Dyadic First-Order Logic in Coq
J
Jacobsen, Frederik Krogsdal	Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
Jakubův, Jan	The Isabelle ENIGMA
Jeannin, Jean-Baptiste	Dandelion: Certified Approximations of Elementary Functions
K
Kaliszyk, Cezary	The Isabelle ENIGMA Formalizing the set of primes as an alternative to the DPRM theorem (short paper)
Kanabar, Hrutvik	Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification
Karayel, Emin	Formalization of Randomized Approximation Algorithms for Frequency Moments
Kavvos, Alex	Deeper Shallow Embeddings
Kirst, Dominik	Undecidability of Dyadic First-Order Logic in Coq Computational Back-and-Forth Arguments in Constructive Type Theory
Kudryashov, Yury	Formalizing the divergence theorem and the Cauchy integral formula in Lean
Kumar, Ramana	Candle: A Verified Implementation of HOL Light
Kunze, Fabian	Synthetic Kolmogorov Complexity in Coq
L
Lammich, Peter	Refinement of Parallel Algorithms down to LLVM
Lampropoulos, Leonidas	Deeper Shallow Embeddings
Lauermann, Nils	Synthetic Kolmogorov Complexity in Coq
Lewis, Robert	Formalized functional analysis with semilinear maps
Lv, Yi	Compositional Verification of Interacting Systems using Event Monads
M
Macbeth, Heather	Formalized functional analysis with semilinear maps
Magaud, Nicolas	Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof Assistant
Mehta, Bhavik	Formalizing Szemerédi's Regularity Lemma in Lean
Moss, Eliot	Mechanizing Soundness of Off-Policy Evaluation
Myreen, Magnus	Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification Candle: A Verified Implementation of HOL Light
N
Norrish, Michael	Mechanizing Soundness of Off-Policy Evaluation Kalas: A Verified, End-to-End Compiler for a Choreographic Language
O
Olšák, Miroslav	The Isabelle ENIGMA
P
Paulson, Lawrence C.	Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics
Pestun, Vasily	Formalization of a Stochastic Approximation Theorem
Philipoom, Jade	Accelerating Verified-Compiler Development with a Verified Rewriting Engine
Piepenbrock, Jelle	The Isabelle ENIGMA
Poddar-Agrawal, Miraya	Accelerating Verified-Compiler Development with a Verified Rewriting Engine Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
Prinz, Jacob	Deeper Shallow Embeddings
Pąk, Karol	Formalizing the set of primes as an alternative to the DPRM theorem (short paper)
Q
Qu, Weihao	Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
S
Sakaguchi, Kazuhiko	Reflexive tactics for algebra, revisited
Sewell, Thomas	Candle: A Verified Implementation of HOL Light
Shaker, James	Kalas: A Verified, End-to-End Compiler for a Choreographic Language
Shinnar, Avraham	Formalization of a Stochastic Approximation Theorem
Stoughton, Alley	Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
T
Tekriwal, Mohit	Dandelion: Certified Approximations of Elementary Functions
Thomas, Philip	Mechanizing Soundness of Off-Policy Evaluation
Trager, Barry	Formalization of a Stochastic Approximation Theorem
U
Urban, Josef	The Isabelle ENIGMA
V
Vajjha, Koundinya	Formalization of a Stochastic Approximation Theorem
Volkova, Anastasia	Dandelion: Certified Approximations of Elementary Functions
Vukmirović, Petar	Seventeen Provers under the Hammer
W
Wang, Shuling	Compositional Verification of Interacting Systems using Event Monads
Wenzel, Makarius	Seventeen Provers under the Hammer
X
Xia, Bican	Compositional Verification of Interacting Systems using Event Monads
Y
Yeager, Jared	Mechanizing Soundness of Off-Policy Evaluation
Z
Zhan, Bohua	(Invited) User Interface Design in the HolPy Theorem Prover Compositional Verification of Interacting Systems using Event Monads
Zhao, Gehang	Compositional Verification of Interacting Systems using Event Monads
Zimmermann, Théo	Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
Å
Åman Pohjola, Johannes	A Verified Cyclicity Checker Kalas: A Verified, End-to-End Compiler for a Choreographic Language

Disclaimer | Powered by EasyChair Smart Program