7 citations · 25 across the 19 of their papers we have counts for
4 papers · 1 filter
Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
Yutaka Nagashima
Proof assistants offer tactics to apply proof by induction, but these tactics rely on inputs given by human engineers. To automate this laborious process, we developed SeLFiE, a bo…
Faster Smarter Induction in Isabelle/HOL
Yutaka Nagashima
Proof by induction plays a critical role in formal verification and mathematics at large. However, its automation remains as one of the long-standing challenges in Computer Science…
Close Encounters of the Higher Kind Emulating Constructor Classes in Standard ML
Yutaka Nagashima, Liam O'Connor
We implement a library for encoding constructor classes in Standard ML, including elaboration from minimal definitions, and automatic instantiation of superclasses.
COGENT: Certified Compilation for a Functional Systems Language
Liam O'Connor, Christine Rizkallah, Zilin Chen +8
We present a self-certifying compiler for the COGENT systems language. COGENT is a restricted, polymorphic, higher-order, and purely functional language with linear types and witho…