“A Case for Lightweight Interfaces in Coq,” authored by David Swasey, Paolo G. Giarrusso, and Gregory Malecha of BedRock Systems, Inc., provides an overview of Coq, including three approaches and their advantages and disadvantages.
Click the below to download a copy of the paper.
