APLAS 2019 (series) / Research Papers /
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Tue 3 Dec 2019 11:30 - 12:00 at Bali Room - Language Design and Implementation Chair(s): Sandrine Blazy
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
Tue 3 Dec
Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
10:30 - 12:00 | Language Design and ImplementationResearch Papers at Bali Room Chair(s): Sandrine Blazy Univ Rennes- IRISA | ||
10:30 30mTalk | Lightweight Functional Logic Meta-Programming Research Papers Nada Amin Harvard University, William E. Byrd University of Alabama at Birmingham, USA, Tiark Rompf Purdue University | ||
11:00 30mTalk | Mimalloc: Free List Sharding in Action Research Papers | ||
11:30 30mTalk | LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL Research Papers Yutaka Nagashima Data61, Australia |