There are type equivalences that can be automatically inferred via algebraic bijections on finite sets we learn in middle school - product (a,b), sum (a|b), and exponential (a->b) - more precise data structures (combinatorial species), and known constraints of allowed functions.
I started research on this in the domain of protein folding equivalences, coming up with https://oeis.org/A186202 - hilarious aside that Laci Babai rejected my journal submission then went and used the sub-optimal n! search as the main subroutine in his latest graph isomorphism paper. 😅
I then started exploring black-box properties of sets of small finite functions, not just permutations: Endoscope. Since the 1970s McKay in the domain of graphs has used black box properties to speed up equivalence checking.
I am a complete noob at Coq - I'm also not sure if Coq is the best language - I like interfaces like SMT-LIB that you can shell out to or wrap in Coq/Python. Artist time is more valuable than computer time
I'm also a fan of Souper and Enzyme - for systems scale proofs LLVM IR is a useful domain language. There are also new tools like CodeQL for AST linting to extract just the parts of code we want to run proofs/transforms on.
Happy to help adding more functionality for combinatorial bijections, generating benchmarks, performance improvement with a systems language or hardware acceleration, and writing linters over C/C++/Rust/LLVM IR/ELF/Mach-O or /proc/ (Where Linux stores information about a running program - halting problem and all that, sometimes you have to run the code) that use this library.
There are type equivalences that can be automatically inferred via algebraic bijections on finite sets we learn in middle school - product (a,b), sum (a|b), and exponential (a->b) - more precise data structures (combinatorial species), and known constraints of allowed functions.
I started research on this in the domain of protein folding equivalences, coming up with https://oeis.org/A186202 - hilarious aside that Laci Babai rejected my journal submission then went and used the sub-optimal n! search as the main subroutine in his latest graph isomorphism paper. 😅
I then started exploring black-box properties of sets of small finite functions, not just permutations: Endoscope. Since the 1970s McKay in the domain of graphs has used black box properties to speed up equivalence checking.
I am a complete noob at Coq - I'm also not sure if Coq is the best language - I like interfaces like SMT-LIB that you can shell out to or wrap in Coq/Python. Artist time is more valuable than computer time
I'm also a fan of Souper and Enzyme - for systems scale proofs LLVM IR is a useful domain language. There are also new tools like CodeQL for AST linting to extract just the parts of code we want to run proofs/transforms on.
Happy to help adding more functionality for combinatorial bijections, generating benchmarks, performance improvement with a systems language or hardware acceleration, and writing linters over C/C++/Rust/LLVM IR/ELF/Mach-O or /proc/ (Where Linux stores information about a running program - halting problem and all that, sometimes you have to run the code) that use this library.
Combinatorial Species and Labeled Structures Functional Algebra for Middle School Students Seven Trees in One The Music of Streams Clowns to the Left of Me, Jokers to the Right Compositional Equality Succinct Representations of Permutations and Functions Efficient Parallel CKY Parsing on GPUs Let's Build a High Performance Fuzzer with GPUs