Tests and Proofs for Enumerative Combinatorics

DOI10.1007/978-3-319-41135-4_4zbMath1348.68217OpenAlexW2477422474MaRDI QIDQ2827441

Richard Genestier, Alain Giorgetti, Catherine Dubois

Publication date: 19 October 2016

Published in: Tests and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-41135-4_4

Mathematics Subject Classification ID

Related Items (1)

Tests and proofs for custom data generators

Uses Software

• Coq
• Nitpick
• PVS
• Haskell
• FocalTest
• OEIS
• QuickCheck
• SmallCheck
• QuickChick
• GitHub
• Mathematical Components

Cites Work

• Unnamed Item
• Designing and proving correct a convex hull algorithm with hypermaps in Coq
• Patterns in permutations and words.
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
• Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
• Graphs on surfaces and their applications. Appendix by Don B. Zagier
• Design and formal proof of a new optimal image segmentation program with hypermaps
• Foundational Property-Based Testing
• The Four Colour Theorem: Engineering of a Formal Proof
• Combinatorial Oriented Maps
• The New Quickcheck for Isabelle
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder

This page was built for publication: Tests and Proofs for Enumerative Combinatorics