[TYPES/announce] New Software Foundations Volume on Random Testing in Coq

Leonidas Lampropoulos llamp at seas.upenn.edu
Wed Aug 29 12:03:06 EDT 2018


We are pleased to announce the release of a new fourth volume in the Software Foundations series, entitled QuickChick: Property-Based Testing in Coq.

https://softwarefoundations.cis.upenn.edu/qc-current/index.html

This new volume describes QuickChick, a property-based random testing tool for Coq, and introduces techniques for combining random testing with formal specification and proof in the Coq ecosystem. The combination enables Coq users to quickly debug theorems and definitions before embarking on manual proof efforts.  Basic knowledge of Coq (e.g., from Logical Foundations, Volume 1 of Software Foundations) is assumed; property-based testing is introduced from scratch.

For a semester course based on Software Foundations, this volume can serve as a basis for a short series of 3 or 4 lectures, following Logical Foundations and before proceeding to either Programming Language Foundations (Volume 2) or Verified Functional Algorithms (Volume 3). This will allow students to leverage random testing when working on the exercises of the more advanced material.

We hope you enjoy this volume and look forward to any feedback you may have.

       — Leo and Benjamin

Leonidas Lampropoulos
llamp at seas.upenn.edu<mailto:llamp at seas.upenn.edu>

Benjamin C. Pierce
bcpierce at cis.upenn.edu<mailto:bcpierce at cis.upenn.edu>

[cid:324a9b02-44e5-40a4-a2f8-75d9894c1e9a]

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20180829/eaceb245/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Cover.png
Type: image/png
Size: 112694 bytes
Desc: Cover.png
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20180829/eaceb245/attachment-0001.png>


More information about the Types-announce mailing list