Talk Keyword Index

TALK KEYWORD INDEX

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

Shortcuts: A C D E F G H I J L M N O P R S T V

A
Amortized Complexity	Amortized Complexity Verified
Automata	The CAVA Automata Library
C
Central Limit Theorem	A formally verified proof of the Central Limit Theorem
Certifying Algorithms	A Simpl Shortest Path Checker Verification
code generation	Towards abstract and executable multivariate polynomials in Isabelle
computer algebra	Towards abstract and executable multivariate polynomials in Isabelle
Consistency	From Types to Sets in Isabelle/HOL
D
definitional package	Primitively (Co)recursive Definitions for Isabelle/HOL
E
events API	Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract)
F
Formal verification	A Simpl Shortest Path Checker Verification
functional programming	Programming TLS in Isabelle/HOL
G
graph theory	A Simpl Shortest Path Checker Verification
Gödel's incompleteness theorem	Proving Gödel’s Incompleteness Theorems
H
higher-order logic	Primitively (Co)recursive Definitions for Isabelle/HOL
HOL	From Types to Sets in Isabelle/HOL
I
interactive theorem proving	A formally verified proof of the Central Limit Theorem
internalization of type classes	From Types to Sets in Isabelle/HOL
IPC API	Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract)
Isabelle	Towards abstract and executable multivariate polynomials in Isabelle Pattern-based Subterm Selection In Isabelle From Types to Sets in Isabelle/HOL Proving Gödel’s Incompleteness Theorems Programming TLS in Isabelle/HOL Towards Structured Proofs for Program Verification (Ongoing Work) Isabelle/jEdit NEWS
Isabelle proof assistant	A formally verified proof of the Central Limit Theorem
Isabelle/HOL	A Simpl Shortest Path Checker Verification Primitively (Co)recursive Definitions for Isabelle/HOL
isar	Towards Structured Proofs for Program Verification (Ongoing Work)
J
jEdit	Isabelle/jEdit NEWS
L
Lifting	From Types to Sets in Isabelle/HOL
local typedef	From Types to Sets in Isabelle/HOL
LTL Model Checking	The CAVA Automata Library
M
MILS (multiple independent levels of security)	Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract)
model	From Types to Sets in Isabelle/HOL
Monad	Programming TLS in Isabelle/HOL
N
network protocol	Programming TLS in Isabelle/HOL
nominal	Proving Gödel’s Incompleteness Theorems
O
Object Oriented Design	The CAVA Automata Library
P
polynomial	Towards abstract and executable multivariate polynomials in Isabelle
program verification	Towards Structured Proofs for Program Verification (Ongoing Work)
Prover IDE	Isabelle/jEdit NEWS
R
refinement	Towards abstract and executable multivariate polynomials in Isabelle
Rewriting	Pattern-based Subterm Selection In Isabelle
S
separation kernel	Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended Abstract)
set-based theorems	From Types to Sets in Isabelle/HOL
Shortest Path	A Simpl Shortest Path Checker Verification
SSReflect	Pattern-based Subterm Selection In Isabelle
structured proof	Towards Structured Proofs for Program Verification (Ongoing Work)
Subterm selection	Pattern-based Subterm Selection In Isabelle
T
theorem proving	Amortized Complexity Verified
Transfer	From Types to Sets in Isabelle/HOL
type-based theorems	From Types to Sets in Isabelle/HOL
V
VCG	Towards Structured Proofs for Program Verification (Ongoing Work)
verification	Amortized Complexity Verified
verification condition generator	Towards Structured Proofs for Program Verification (Ongoing Work)