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

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
30m
Talk
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
30m
Talk
Mimalloc: Free List Sharding in Action
Research Papers
Daan Leijen Microsoft Research, USA, Ben Zorn Microsoft, Leonardo de Moura Microsoft Research, n.n.
11:30
30m
Talk
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Research Papers
Yutaka Nagashima Data61, Australia