FLOC 2022: FEDERATED LOGIC CONFERENCE 2022

This page contains an index consisting of author-provided keywords.

A
ACL2(r)	A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(r)
ad-hoc overloading	A Verified Cyclicity Checker
additive combinatorics	Formalizing Szemerédi's Regularity Lemma in Lean
adversary argument	Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
algebraic hierarchy	Use and abuse of instance parameters in the Lean mathematical library
algebraic number theory	Formalizing the ring of adèles of a global field
algebraic structures	Reflexive tactics for algebra, revisited
automated theorem proving	The Isabelle ENIGMA
automatic test-case reduction	Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
Automatic theorem proving	Seventeen Provers under the Hammer
B
back-and-forth method	Computational Back-and-Forth Arguments in Constructive Type Theory
Banach-Tarski	A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(r)
bug minimizer	Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
C
canonical structures	Reflexive tactics for algebra, revisited
Cauchy integral formula	Formalizing the divergence theorem and the Cauchy integral formula in Lean
Cauchy-Goursat theorem	Formalizing the divergence theorem and the Cauchy integral formula in Lean
certificate checking	Dandelion: Certified Approximations of Elementary Functions
choreography	Kalas: A Verified, End-to-End Compiler for a Choreographic Language
class field theory	Formalizing the ring of adèles of a global field
Combinatorics	Formalizing Szemerédi's Regularity Lemma in Lean Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics
compilation	Kalas: A Verified, End-to-End Compiler for a Choreographic Language
Compiler verification	Accelerating Verified-Compiler Development with a Verified Rewriting Engine
Completeness	Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
complex analysis	Formalizing the divergence theorem and the Cauchy integral formula in Lean
Compositional Verification	Compositional Verification of Interacting Systems using Event Monads
computability theory	Synthetic Kolmogorov Complexity in Coq
computable isomorphisms	Computational Back-and-Forth Arguments in Constructive Type Theory
concentration inequalities	Mechanizing Soundness of Off-Policy Evaluation
concurrency	Kalas: A Verified, End-to-End Compiler for a Choreographic Language
Concurrent Separation Logic	Refinement of Parallel Algorithms down to LLVM
constructive matemathics	Synthetic Kolmogorov Complexity in Coq
constructive type theory	Synthetic Kolmogorov Complexity in Coq Computational Back-and-Forth Arguments in Constructive Type Theory
Coq	Synthetic Kolmogorov Complexity in Coq Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof Assistant Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq Computational Back-and-Forth Arguments in Constructive Type Theory Undecidability of Dyadic First-Order Logic in Coq The Zoo of Lambda-Calculus Reduction Strategies, and Coq Reflexive tactics for algebra, revisited (Invited) Modelling and Verifying Properties of Biological Neural Networks
cryptography	Accelerating Verified-Compiler Development with a Verified Rewriting Engine
cyclicity	A Verified Cyclicity Checker
D
debugging	Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq
Deep Embedding	Deeper Shallow Embeddings
definitions	A Verified Cyclicity Checker
dependent type theory	Deeper Shallow Embeddings Use and abuse of instance parameters in the Lean mathematical library
diophantine sets	Formalizing the set of primes as an alternative to the DPRM theorem (short paper)
divergence theorem	Formalizing the divergence theorem and the Cauchy integral formula in Lean
DPRM theorem	Formalizing the set of primes as an alternative to the DPRM theorem (short paper)
E
EasyCrypt	Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
elementary functions	Dandelion: Certified Approximations of Elementary Functions
Elpi	Reflexive tactics for algebra, revisited
Events	Compositional Verification of Interacting Systems using Event Monads
F
finite models	Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof Assistant
first-order logic	Undecidability of Dyadic First-Order Logic in Coq Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
formal mathematics	Formalizing the ring of adèles of a global field
formal proof	Formalizing Szemerédi's Regularity Lemma in Lean
Formal Proof Techniques	Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics
formal verification	Formalization of a Stochastic Approximation Theorem Formalization of Randomized Approximation Algorithms for Frequency Moments
formalization	Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof Assistant Formalizing Szemerédi's Regularity Lemma in Lean
formalization of mathematics	Use and abuse of instance parameters in the Lean mathematical library
Frequency Moments	Formalization of Randomized Approximation Algorithms for Frequency Moments
functional analysis	Formalized functional analysis with semilinear maps
G
Gauge integral	Formalizing the divergence theorem and the Cauchy integral formula in Lean
graph theory	Formalizing Szemerédi's Regularity Lemma in Lean
Green's theorem	Formalizing the divergence theorem and the Cauchy integral formula in Lean
H
Higher-order logic	Candle: A Verified Implementation of HOL Light
Hilbert space	Formalized functional analysis with semilinear maps
hoare logic	Compositional Verification of Interacting Systems using Event Monads
HOL Light	Candle: A Verified Implementation of HOL Light
HOL4	Dandelion: Certified Approximations of Elementary Functions Mechanizing Soundness of Off-Policy Evaluation Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification
I
Interactive Theorem Proving	The Isabelle ENIGMA Dandelion: Certified Approximations of Elementary Functions Seventeen Provers under the Hammer
ISA specification	Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification
Isabelle	Refinement of Parallel Algorithms down to LLVM
Isabelle Sledgehammer	The Isabelle ENIGMA
Isabelle/HOL	Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics A Verified Cyclicity Checker Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL Formalization of Randomized Approximation Algorithms for Frequency Moments
K
Kolmogorov complexity	Synthetic Kolmogorov Complexity in Coq
L
lambda calculus	The Zoo of Lambda-Calculus Reduction Strategies, and Coq
Lean	Formalizing Szemerédi's Regularity Lemma in Lean Formalized functional analysis with semilinear maps Formalizing the ring of adèles of a global field
Lean prover	Use and abuse of instance parameters in the Lean mathematical library
Linear Algebra	Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics Formalized functional analysis with semilinear maps
LLVM	Refinement of Parallel Algorithms down to LLVM
lower bound	Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
M
machine learning	The Isabelle ENIGMA
Mathematical Components	Reflexive tactics for algebra, revisited
Mathematical Formalisation	Formalising Fisher’s Inequality: Formal Linear Algebraic Techniques in Combinatorics
Mathematics	Formalized functional analysis with semilinear maps
mathlib	Formalizing the ring of adèles of a global field
measure theory	Mechanizing Soundness of Off-Policy Evaluation
Mizar	Formalizing the set of primes as an alternative to the DPRM theorem (short paper)
model checking	(Invited) Modelling and Verifying Properties of Biological Neural Networks
models of computation	Synthetic Kolmogorov Complexity in Coq
N
Neuronal networks	(Invited) Modelling and Verifying Properties of Biological Neural Networks
non-termination	A Verified Cyclicity Checker
O
Optimization Algorithms	Formalization of a Stochastic Approximation Theorem
P
packed classes	Reflexive tactics for algebra, revisited
Parallel Sorting Algorithms	Refinement of Parallel Algorithms down to LLVM
polynomial approximation	Dandelion: Certified Approximations of Elementary Functions
Premise Selection	The Isabelle ENIGMA
Probability Theory	Formalization of a Stochastic Approximation Theorem
Program Verification	Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification
projective geometry	Proof Pearl: Formalizing Spreads and Packings of the Smallest Projective Space PG(3,2) using the Coq Proof Assistant
Proof assistants	Seventeen Provers under the Hammer (Invited) User Interface Design in the HolPy Theorem Prover
Proof automation	(Invited) User Interface Design in the HolPy Theorem Prover
proof by reflection	Reflexive tactics for algebra, revisited
Prover	Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
Q
query model	Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
R
random numbers	Synthetic Kolmogorov Complexity in Coq
Randomized Algorithms	Formalization of Randomized Approximation Algorithms for Frequency Moments
Reduction strategies	The Zoo of Lambda-Calculus Reduction Strategies, and Coq
Refinement	Refinement of Parallel Algorithms down to LLVM
reinforcement learning	Mechanizing Soundness of Off-Policy Evaluation
Remez algorithm	Dandelion: Certified Approximations of Elementary Functions
rewriting engines	Accelerating Verified-Compiler Development with a Verified Rewriting Engine
Rotations	A Complete, Mechanically-Verified Proof of the Banach-Tarski Theorem in ACL2(r)
Roth's Theorem	Formalizing Szemerédi's Regularity Lemma in Lean
S
SeCaV	Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
semilinear	Formalized functional analysis with semilinear maps
shallow embedding	Deeper Shallow Embeddings
soundness	Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL
statistics	Mechanizing Soundness of Off-Policy Evaluation
Stochastic Approximation	Formalization of a Stochastic Approximation Theorem
Stochastic Processes	Formalization of a Stochastic Approximation Theorem
synthetic computability	Undecidability of Dyadic First-Order Logic in Coq
synthetic computability theory	Synthetic Kolmogorov Complexity in Coq
Szemerédi's Regularity Lemma	Formalizing Szemerédi's Regularity Lemma in Lean
T
Theorem prover soundness	Candle: A Verified Implementation of HOL Light
theorem proving	(Invited) Modelling and Verifying Properties of Biological Neural Networks
type classes	Use and abuse of instance parameters in the Lean mathematical library
U
Undecidability	Undecidability of Dyadic First-Order Logic in Coq
upper bound	Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
User interface	(Invited) User Interface Design in the HolPy Theorem Prover
λ
λProlog	Reflexive tactics for algebra, revisited

Disclaimer | Powered by EasyChair Smart Program