coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] New Software Foundations Volume on Random Testing in Coq, Leonidas Lampropoulos, 08/29/2018
Archive powered by MHonArc 2.6.18.