FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

C
CDCL	A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) (PDF, talk)
code generation	Lazy Algebraic Types in Isabelle/HOL (PDF, talk)
Complexity	Formal Verification of Bounds for the LLL Basis Reduction Algorithm (PDF, talk)
D
denotational semantics	Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (PDF, talk)
Diophantine equations	Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
DPRM Theorem	Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
Drawing trees	Drawing Trees (PDF)
F
first-order logic	Substitutionless First-Order Logic: A Formal Soundness Proof (PDF, talk)
formal verification	Drawing Trees (PDF)
formalization	Substitutionless First-Order Logic: A Formal Soundness Proof (PDF, talk)
H
Hilbert's tenth problem	Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
HOL	Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (PDF, talk)
I
Isabelle	Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk) Further Scaling of Isabelle Technology (PDF, talk) The remote_build Tool (PDF, talk) Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (PDF, talk)
Isabelle/HOL	Formal Verification of Bounds for the LLL Basis Reduction Algorithm (PDF, talk) Drawing Trees (PDF) PaMpeR: A Proof Method Recommendation System for Isabelle/HOL (PDF, talk)
IsaSAT	A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) (PDF, talk)
L
Lattice Basis Reduction	Formal Verification of Bounds for the LLL Basis Reduction Algorithm (PDF, talk)
Layout algorithm	Drawing Trees (PDF)
lazy evaluation	Lazy Algebraic Types in Isabelle/HOL (PDF, talk)
M
Machine Learning	PaMpeR: A Proof Method Recommendation System for Isabelle/HOL (PDF, talk)
P
pattern matching	Lazy Algebraic Types in Isabelle/HOL (PDF, talk)
Program Verification	Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (PDF, talk)
Proof Method Recommendation	PaMpeR: A Proof Method Recommendation System for Isabelle/HOL (PDF, talk)
Proof Mining	PaMpeR: A Proof Method Recommendation System for Isabelle/HOL (PDF, talk)
Proof System	Substitutionless First-Order Logic: A Formal Soundness Proof (PDF, talk)
R
recursively enumerable	Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle (PDF, talk)
refinement	A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) (PDF, talk)
Regression Tree	PaMpeR: A Proof Method Recommendation System for Isabelle/HOL (PDF, talk)
remote build	The remote_build Tool (PDF, talk)
S
SAT Solver	A Verified SAT Solver with Watched Literals Using Imperative HOL (Extended Abstract) (PDF, talk)
Scaling	Further Scaling of Isabelle Technology (PDF, talk)
Soundness	Substitutionless First-Order Logic: A Formal Soundness Proof (PDF, talk)
Substitution	Substitutionless First-Order Logic: A Formal Soundness Proof (PDF, talk)
T
Technology	Further Scaling of Isabelle Technology (PDF, talk)
tool	The remote_build Tool (PDF, talk)
U
Unifying Theories of Programming	Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study (PDF, talk)

Disclaimer | Powered by EasyChair Smart Program