ISABELLE 2014 PAPERS (UNREFEREED): KEYWORD INDEX

Papers Papers with Abstracts Preface Author Index Keyword Index Additional files

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

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