University of Udine University of Udine

Internal Adequacy of Bookkeeping in Coq


Alberto Ciaffaglione, Ivan Scagnetto

We provide an alternative, shallow encoding version of Sistem F<'s algorithmic subtyping,
and prove its adequacy w.r.t. our deep one, used to address the POPLmark Challenge.

Our research has been published at LFMTP 2014, and the Coq script is available [here].


Last updated: May 6, 2014