C-CoRN
From MaRDI portal
Software:18827
swMATH6752MaRDI QIDQ18827FDOQ18827
Author name not available (Why is that?)
Cited In (39)
- Constructive analysis, types and exact real numbers
- User interaction with the Matita proof assistant
- A Wiki for Mizar: Motivation, Considerations, and Initial Prototype
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- Type classes for mathematics in type theory
- Finite Groups Representation Theory with Coq
- Views of Pi: definition and computation
- Large Formal Wikis: Issues and Solutions
- 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
- Type classes for efficient exact real arithmetic in Coq
- Developing the Algebraic Hierarchy with Type Classes in Coq
- Formal Verification of Exact Computations Using Newton’s Method
- Quantitative continuity and Computable Analysis in Coq
- Proof assistants: history, ideas and future
- 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
- Title not available (Why is that?)
- Working with Mathematical Structures in Type Theory
- A computer-verified monadic functional implementation of the integral
- 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
- A Formal Proof of Cauchy’s Residue Theorem
This page was built for software: C-CoRN
