C-CoRN
From MaRDI portal
Software:18827
swMATH6752MaRDI QIDQ18827FDOQ18827
Author name not available (Why is that?)
Cited In (39)
- Type classes for efficient exact real arithmetic in \textsc{Coq}
- Constructive analysis, types and exact real numbers
- User interaction with the Matita proof assistant
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- A formal proof of Cauchy's residue theorem
- Type classes for mathematics in type theory
- Finite Groups Representation Theory with Coq
- Formalization \textit{of} quantum protocols using Coq
- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
- Certified Exact Transcendental Real Number Computation in Coq
- 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
- 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
- Quantitative continuity and Computable Analysis in Coq
- Proof assistants: history, ideas and future
- 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
- Automated Machine-Checked Hybrid System Safety Proofs
- Automating Side Conditions in Formalized Partial Functions
- Title not available (Why is that?)
- Formalization of real analysis: a survey of proof assistants and libraries
- Working with Mathematical Structures in Type Theory
- A computer-verified monadic functional implementation of the integral
- Developing the algebraic hierarchy with type classes in Coq
- Formal proofs for theoretical properties of Newton's method
- Coquelicot: a user-friendly library of real analysis for Coq
- Mathematical Knowledge Management
- Constructive hybrid games
- The Picard Algorithm for Ordinary Differential Equations in Coq
This page was built for software: C-CoRN
