Tests and proofs for custom data generators
From MaRDI portal
Publication:1624592
DOI10.1007/s00165-018-0459-1zbMath1425.68373OpenAlexW2816677331WikidataQ60691913 ScholiaQ60691913MaRDI QIDQ1624592
Catherine Dubois, Alain Giorgetti
Publication date: 16 November 2018
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-018-0459-1
permutationscombinatorial enumerationlogic programmingrandom testingrooted mapsinteractive theorem provingbounded-exhaustive testing
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Designing and proving correct a convex hull algorithm with hypermaps in Coq
- A permutation code preserving a double Eulerian bistatistic
- Patterns in permutations and words.
- A new Euler-Mahonian constructive bijection
- 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
- Gray code for permutations with a fixed number of cycles
- Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof
- Graphs on surfaces and their applications. Appendix by Don B. Zagier
- Recent progress in enumeration of hypermaps
- Constructing permutation arrays from groups
- Lehmer code transforms and Mahonian statistics on permutations
- A verified algorithm enumerating event structures
- Satisfiability modulo bounded checking
- Counting rooted maps by genus. I
- Design and formal proof of a new optimal image segmentation program with hypermaps
- Tests and Proofs for Enumerative Combinatorics
- Formal Matrix Integrals and Combinatorics of Maps
- Foundational Property-Based Testing
- Ranking/Unranking of Lambda Terms with Compressed de Bruijn Indices
- Quantum contextual finite geometries from dessins d'enfants
- The Four Colour Theorem: Engineering of a Formal Proof
- Combinatorial Oriented Maps
- A Combinatorial Interpretation of the Seidel Generation of Genocchi Numbers
- The New Quickcheck for Isabelle
- Why3 — Where Programs Meet Provers
- Pragmatic Quotient Types in Coq
- Beginner's luck: a language for property-based generators
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
This page was built for publication: Tests and proofs for custom data generators
