The following pages link to Canonical Big Operators (Q3543652):
Displaying 22 items.
- Completeness and decidability results for CTL in constructive type theory (Q287375) (← links)
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952) (← links)
- Formal proofs of rounding error bounds. With application to an automatic positive definiteness check (Q2013318) (← links)
- Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
- Formalization of Shannon's theorems (Q2352494) (← links)
- Formally verified certificate checkers for hardest-to-round computation (Q2352500) (← links)
- Trusting computations: a mechanized proof from partial differential equations to actual program (Q2398899) (← links)
- A Coq formalization of Lebesgue integration of nonnegative functions (Q2673304) (← links)
- A Certified Reduction Strategy for Homological Image Processing (Q2946732) (← links)
- Computational Complexity Via Finite Types (Q2946764) (← links)
- Point-Free, Set-Free Concrete Linear Algebra (Q3088000) (← links)
- Formal proofs for theoretical properties of Newton's method (Q3094171) (← links)
- Hints in Unification (Q3183522) (← links)
- Packaging Mathematical Structures (Q3183538) (← links)
- Finite Groups Representation Theory with Coq (Q3637300) (← links)
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis (Q5048989) (← links)
- Incidence Simplicial Matrices Formalized in Coq/SSReflect (Q5200106) (← links)
- Implementing type theory in higher order constraint logic programming (Q5236551) (← links)
- A formal proof of the expressiveness of deep learning (Q5915784) (← links)
- A formal proof of the expressiveness of deep learning (Q5919583) (← links)
- Measure construction by extension in dependent type theory with application to integration (Q6050768) (← links)
- Formally-verified round-off error analysis of Runge-Kutta methods (Q6149594) (← links)
