Logarithm and Program Testing
summary
Proposes a mechanical monomorphization that, for prenex System F with products, sums, functions and strictly positive inductive types, computes a special type and finite inputs (called A star and E star) so that checking a reference F and an implementation F' on those inputs implies equality on all instantiations. The key calculation is a logarithm calculation that yields how many distinct inhabitants are needed; an implementation in Haskell plugs into QuickCheck/SmallCheck and artifacts are available. The method sometimes overestimates (gives Nat where Unit would suffice).
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:20Test cases
- 5:57Generalized annual projection
- 8:48Polymorphic functions
- 9:57Theorem
- 11:30Expanding the logarithm
- 12:58Previous works
- 14:24Conclusion
- 17:34Questions
related talks
52mProgramming and Math
46mTesting in the world of Functional Programming
01h 02mTesting Boolean Functions
14mVerify, but test: extracting property-based tests from F* specifications
28mLanguage Support for Property-Based Testing
44mTypes and Property Tests for Software Resiliency
32mGenerative Testing: Properties, State and Beyond
51mWhen Types are Not Enough