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 |