Author:Rustan Leino

Publications
Well-founded Functions and Extreme Predicates in Dafny: A Tutorial Rustan Leino In:IWIL-2015. 11th International Workshop on the Implementation of Logics
Compiling Hilbert's epsilon operator Rustan Leino In:LPAR-20. 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations

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.