7 citations · 25 across the 19 of their papers we have counts for
Showing 2016Show all
3 papers · 1 filter
cs.PL2016★ 3 cited
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.
cs.LO2016★ 2 cited
A Proof Strategy Language and Proof Script Generation for Isabelle/HOL
Yutaka Nagashima, Ramana Kumar
We introduce a language, PSL, designed to capture high level proof strategies in Isabelle/HOL. Given a strategy and a proof obligation, PSL's runtime system generates and combines…
cs.PL2016★ 4 cited
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…