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