Talk Keyword Index

TALK KEYWORD INDEX

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

Shortcuts: C D F H I L M P R S T U

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