Skip to Content.
Sympa Menu

coq-club - [Coq-Club] New Software Foundations Volume on Random Testing in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] New Software Foundations Volume on Random Testing in Coq


Chronological Thread 
  • From: Leonidas Lampropoulos <llamp AT seas.upenn.edu>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] New Software Foundations Volume on Random Testing in Coq
  • Date: Wed, 29 Aug 2018 16:12:07 +0000
  • Accept-language: en-US
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lemonidas_13 AT hotmail.com; spf=Pass smtp.mailfrom=llamp AT seas.upenn.edu; spf=None smtp.helo=postmaster AT mx0b-000c2a01.pphosted.com
  • Ironport-phdr: 9a23:Ptm4ShaYi4sO9Xx2o42fxZv/LSx+4OfEezUN459isYplN5qZr8i8bnLW6fgltlLVR4KTs6sC17KJ9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa/bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjm58axlVAHnhzsGNz4h8WHYlMpwjL5AoBm8oxBz2pPYbJ2JOPZ7eK7WYNEUSndbXstJVyJPHJ6yb5cUD+QPPuhXs4byqkAUrReiCgahHv/jxiNIi3LwwKY00/4hEQbD3AE4GdwBrnPUrNP0NKgPS++117TDwzPZYPNTwTf98o/IcggmofGRWbJwdtHRwlQoGgPBilWfs4nlPyuO2+QWrWeU9fFgWfiyi24/tQ5xpD6vyt0yhYbUm4IY01bJ/jh3zoYyIN23Uk97Ydi8HZtNryGVKY12QsU4T252pSk617sLsoO4cigS0Jkr2hHSZv+df4SV4x/uWvydLSp4iX9lYr6yiRe//VCvx+HgTMW51FRHojBYntTPtX0BzQHf58uDR/Z740yvwyyA1xrJ5eFBOU00lbTUK5omwrMok5oSvljPETTvlEnqkKOaalkr9vay5Oj7f7nqvIecN5d0igH5KaQuhtKwDvkiPgcSWGib/Pyw1Lzl/ULnXLVHluA6n6bavZzAOMgWp6C0DxVI3osj6xuzFTmr3dUAkXkCNl1FeRaHj4bzO1HJJfD1FfO/g1C2nzdu3/DLJabhDYvXIXjYirvhYK595FBayAo119xQ+Y9bCqwZLPLpRkDxrMDYDgM+MwGs3+nnD8x92poCVmKLH6+WK7jfsUSI5+IqO+mDfpUZuDf7K/g/5v7hl2U1mVEHffrh4ZxCQ3ehVt9iPk/RNXHrm5IKFXoAlgs4Vu3jzlOYB219fXG3CoYx4Tc6BIu9RaPKQ5i3h6SGwSO8BdUCYmRPD0ikCnrhbMOZQ/oKbmSfLtI3wW9MbqSoV4J0jULmjwT90bcya7OMonRJ56Km78B84qjorT938DV1C8qH1GTUETNvk2oTASIu0aZ550Fx1wXaiPQqs7ljDdVWoshxfEIiL5eFlL56DMz3UwPFONyOTQT+G4j0MXQKVts0huQ2TQN9FtGl1ECR2jryCfpNz+SAXpVsq+TEx3j2PNpwxzDN06xz11Q=

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

Benjamin C. Pierce 

bcpierce AT cis.upenn.edu


JPEG image



  • [Coq-Club] New Software Foundations Volume on Random Testing in Coq, Leonidas Lampropoulos, 08/29/2018

Archive powered by MHonArc 2.6.18.

Top of Page