Author:Rustan Leino
Keyphrases
Choose operator, coinduction, Coinductive predicate, compilation, Encoding for SMT solver, greatest fixpoint, Hilbert's epsilon operator, induction, inductive predicate, least fixpoint, mechanical proof assistant, Russell's definite description operator, Verification-aware programming language.