LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however they did not have a systematic way to encode their expertise. To address this problem, we present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of any problem domain. LiFtEr’s interpreter mechanically checks if a given application of induction tool matches the heuristics, thus transferring the Isabelle experts’ expertise to new Isabelle users.
Tue 3 DecDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
10:30 - 12:00
|Lightweight Functional Logic Meta-Programming|
|Mimalloc: Free List Sharding in Action|
|LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL|
Yutaka Nagashima Data61, Australia