Write a Blog >>
APLAS 2019
Sun 1 - Wed 4 December 2019 Bali, Indonesia
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 Dec
Times are displayed in time zone: (GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi change

10:30 - 12:00: Research Papers - Language Design and Implementation at Bali Room
Chair(s): Sandrine BlazyUniv Rennes- IRISA
aplas-2019-papers10:30 - 11:00
Nada AminHarvard University, William E. ByrdUniversity of Alabama at Birmingham, USA, Tiark RompfPurdue University
aplas-2019-papers11:00 - 11:30
Daan LeijenMicrosoft Research, USA, Ben ZornMicrosoft, Leonardo De MouraMicrosoft Research, n.n.
aplas-2019-papers11:30 - 12:00
Yutaka NagashimaData61, Australia