FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
ITP PAPERS: KEYWORD INDEX
A
Agda
Asynchronous
automated reasoning
B
Bar inductive predicates
Basis Reduction
Biform theories
binary search tree
C
Cached Address Translation
calculational method
Calculational proof
call by push value
Cedille
certificate checking
certified code
Certified execution engine
certified software
Church's type theory
classical realizability
Clause Learning
code generation
coinductive types
common knowledge
complete lattices
Computational Reductions
Context-free Grammars
contextual equivalence
Control parameters
Coq
Correctness by extraction
Cycle finding
D
Databases
datatypes
deductive verification
Dedukti
dependent types
dependently typed programming
Design by contract
domain specific languages
dynamic epistemic logic
Dynamic Programming
E
Economics
epistemic logic
equational theory
Expected Utility
extraction
F
Formal Methods
formal proofs
formal verification
Formalisation
functional programming
functor
G
Game Theory
graph minor theorem
graph theory
H
hammers
handwriting
handwritten mathematics
Hardware model
hardware verification
Higher-Ranked Polymorphism
HOL
HOL Light
homogeneous linear diophantine equations
HW-SW interface
I
IDE
implicative algebras
induction principle
inductive datatypes
interactive theorem proving
Isabelle
Isabelle/HOL
Isabelle/HOL Theorem Proving
K
KeY
L
lambda-encodings
large libraries
Linear Programming
loop unrolling
M
machine words
Markov decision processes
Master Theorem
mathematical proof
Mathematics
mechanized mathematics
Memoization
Memory
meta programming
meta-programming
Metareasoning
MIPS TLB
model checking
model-based testing
N
normal form bisimulation
O
observational equivalence
Operating System Verification
optimizations
P
Parametricity
Partial algorithms in Coq
Polynomial Factorization
polytyptic programming
Post Correspondence Problem
predecessor function
probabilistic
Probabilistic Timed Automata
probability
Program Verification
proof assistants
proof automation
proof by reflection
proof engineering
proof guidance
proof theory of modal logic
Proof-checker
PVS
Q
Quicksort
Quotation and evaluation
quotients
R
randomised
randomized algorithm
Reasoning about syntax
refinement
Reflection
reification
rewriting
Ring Theory
S
Security
separation logic
Skeptical Approach
software verification
SQL
Ssreflect
string rewriting
strongest postcondition
symbolic computation
T
tactics
tail bound
Teaching computer science with proof assistants
The Coq Proof Assistant
theorem proving
Timed automata
timing transformations
Translation Lookaside Buffer (TLB)
treap
tripos
trusted code base
trusted computing base
Type Inference
type theory
U
Ultrametrics
Undecidability
untyped call by value lambda calculus
Utility Theory
V
validation
Verification
verified compiler
Von Neumann-Morgenstern Utility Theorem
W
watchlist guidance
weakest precondition