Pages that link to "Item:Q3612435"
From MaRDI portal
The following pages link to Fast Reflexive Arithmetic Tactics the Linear Case and Beyond (Q3612435):
Displaying 18 items.
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation (Q1663216) (← links)
- Coquelicot: a user-friendly library of real analysis for Coq (Q2018661) (← links)
- A bi-directional extensible interface between Lean and Mathematica (Q2673306) (← links)
- Extensible and Efficient Automation Through Reflective Tactics (Q2802496) (← links)
- On the Generation of Positivstellensatz Witnesses in Degenerate Cases (Q3088010) (← links)
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses (Q3100209) (← links)
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq (Q3100210) (← links)
- Tactics for Reasoning Modulo AC in Coq (Q3100211) (← links)
- A Short Presentation of Coq (Q3543643) (← links)
- Ready,<tt>Set</tt>, Verify! Applying<tt>hs-to-coq</tt>to real-world Haskell code (Q5018778) (← links)
- Formalizing the Face Lattice of Polyhedra (Q5049001) (← links)
- Sharper and Simpler Nonlinear Interpolants for Program Verification (Q5056007) (← links)
- (Q5094138) (← links)
- Formal Proofs for Nonlinear Optimization (Q5195260) (← links)
- (Q5856420) (← links)
- A formalization of convex polyhedra based on the simplex method (Q5915783) (← links)
- Pourchet’s theorem in action: decomposing univariate nonnegative polynomials as sums of five squares (Q6081964) (← links)
- Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq (Q6611970) (← links)