The following pages link to Extraction in Coq: An Overview (Q3507450):
Displayed 16 items.
- Sorting nine inputs requires twenty-five comparisons (Q899586) (← links)
- A verified framework for higher-order uncurrying optimizations (Q968367) (← links)
- Schulze voting as evidence carrying computation (Q1687758) (← links)
- Formally proving size optimality of sorting networks (Q1694569) (← links)
- Classical misuse attacks on NIST round 2 PQC. The power of rank-based schemes (Q2229273) (← links)
- Formally verifying the solution to the Boolean Pythagorean triples problem (Q2323449) (← links)
- A formally verified compiler back-end (Q2655327) (← links)
- Functional Encryption for Inner Product with Full Function Privacy (Q2798775) (← links)
- A Certified Reduction Strategy for Homological Image Processing (Q2946732) (← links)
- Animating the Formalised Semantics of a Java-Like Language (Q3088008) (← links)
- Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof (Q3453106) (← links)
- Certified Graph View Maintenance with Regular Datalog (Q4559800) (← links)
- (Q5028422) (← links)
- Computer Certified Efficient Exact Reals in Coq (Q5200110) (← links)
- Calculating correct compilers (Q5371953) (← links)
- A Verified LL(1) Parser Generator (Q5875434) (← links)
