Advances in Property-Based Testing for αProlog

James Cheney, Alberto Momigliano, Matteo Pessina

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

αCheck is a light-weight property-based testing tool built on top of αProlog, a logic programming language based on nominal logic. αProlog is particularly suited to the validation of the meta-theory of formal systems, for example correctness of compiler translations involving name-binding, alpha-equivalence and capture-avoiding substitution. In this paper we describe an alternative to the negation elimination algorithm underlying αCheck that substantially improves its effectiveness. To substantiate this claim we compare the checker performances w.r.t. two of its main competitors in the logical framework niche, namely the QuickCheck/Nitpick combination offered by Isabelle/HOL and the random testing facility in PLT-Redex.
Original languageEnglish
Title of host publicationTests and Proofs
Subtitle of host publication10th International Conference, TAP 2016, Held as Part of STAF 2016, Vienna, Austria, July 5-7, 2016, Proceedings
PublisherSpringer International Publishing
Number of pages20
ISBN (Electronic)978-3-319-41135-4
ISBN (Print)978-3-319-41134-7
Publication statusPublished - Jun 2016
Event10th International Conference on Tests & Proofs - Vienna, Austria
Duration: 5 Jul 20167 Jul 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
ISSN (Print)0302-9743


Conference10th International Conference on Tests & Proofs
Abbreviated titleTAP 2016
Internet address

Keywords / Materials (for Non-textual outputs)

  • cs.LO
  • cs.PL


Dive into the research topics of 'Advances in Property-Based Testing for αProlog'. Together they form a unique fingerprint.

Cite this