PADL2021: the first release of SeLFiE
Pre-releaseThis is the accompanying release for our PADL2021 submission. This release contains the interpreter of SeLFiE in PSL/SeLFiE
.
To learn how to install is, read the instructions in PSL/SeLFiE/README.md
.
Proof by induction is a long-standing challenge in Computer Science.
Proof assistants offer tactics to apply proof by induction, but these tactics rely on inputs given by human engineers.
We address this problem with SeLFiE, a domain-specific language to encode experienced users’ expertise on how to apply the induct tactic in Isabelle/HOL: when we apply an induction heuristic written in SeLFiE to an inductive problem and arguments to the induct tactic, the interpreter examines both the syntactic structure of the problem and semantics of the relevant constants to judge whether the arguments to the induct tactic are plausible according to the heuristic.