Cited in
(58)- Mathematical Knowledge Management
- The Picard Algorithm for Ordinary Differential Equations in Coq
- Type classes for efficient exact real arithmetic in \textsc{Coq}
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- Constructive analysis, types and exact real numbers
- User interaction with the Matita proof assistant
- A formal proof of Cauchy's residue theorem
- Type classes for mathematics in type theory
- Computable analysis and notions of continuity in \textsc{Coq}
- Finite Groups Representation Theory with Coq
- Formalization \textit{of} quantum protocols using Coq
- Certified Exact Transcendental Real Number Computation in Coq
- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
- Mathematical Knowledge Management
- A constructive and formal proof of Lebesgue's dominated convergence theorem in the interactive theorem prover Matita
- Axiomatic reals and certified efficient exact real computation
- Mathematical Knowledge Management
- A formal study of Bernstein coefficients and polynomials
- Gappa
- Matita
- Ariadne
- Flocq
- iRRAM
- FoCaL
- AERN
- OpenAxiom
- Coquelicot
- ROSCoq
- RealCertify
- VeriPhy
- ProofPeer
- Algebraic_VCs
- KAD
- Whelp
- Web interfaces for proof assistants
- Mathematical Knowledge Management
- Invariants for the FoCaL language
- Large formal wikis: issues and solutions
- Views of pi: definition and computation
- Formal Verification of Exact Computations Using Newton’s Method
- Quantales
- Transformer semantics
- Proof assistants: history, ideas and future
- Quantitative continuity and Computable Analysis in Coq
- A Wiki for Mizar: motivation, considerations, and initial prototype
- Types for Proofs and Programs
- Affine functions and series with co-inductive real numbers
- Mathematical Knowledge Management
- Formalization of real analysis: a survey of proof assistants and libraries
- Automated Machine-Checked Hybrid System Safety Proofs
- Automating Side Conditions in Formalized Partial Functions
- A computer-verified monadic functional implementation of the integral
- Working with Mathematical Structures in Type Theory
- Developing the algebraic hierarchy with type classes in Coq
- Formal proofs for theoretical properties of Newton's method
- Smooth_Manifolds
- Coquelicot: a user-friendly library of real analysis for Coq
- Constructive hybrid games
This page was built for software: C-CoRN
