| ||||
| ||||
![]() Title:Formalizing Algorithmic Bounds in the Query Model in EasyCrypt Conference:ITP 2022 Tags:adversary argument, EasyCrypt, lower bound, query model and upper bound Abstract: We use the EasyCrypt proof assistant to formalize the adversarial approach to proving lower bounds for computational problems in the query model. This is done using a lower bound game between an algorithm and adversary, in which the adversary answers the algorithm's queries in a way that makes the algorithm issue at least the desired number of queries. A complementary upper bound game is used for proving upper bounds of algorithms; here the adversary incrementally and adaptively realizes an algorithm's input. We prove a natural connection between the lower and upper bound games, and apply our framework to three computational problems, including searching in an ordered list and comparison-based sorting, giving evidence for the generality of our notion of algorithm and the usefulness of our framework. Formalizing Algorithmic Bounds in the Query Model in EasyCrypt ![]() Formalizing Algorithmic Bounds in the Query Model in EasyCrypt | ||||
Copyright © 2002 – 2025 EasyChair |