swMATH6752MaRDI QIDQ18827FDOQ18827
Author name not available (Why is that?)
Official website: http://corn.cs.ru.nl/
Cited In (58)
- Type classes for efficient exact real arithmetic in \textsc{Coq}
- Constructive analysis, types and exact real numbers
- User interaction with the Matita proof assistant
- Quantales
- Transformer semantics
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- A formal proof of Cauchy's residue theorem
- Computable analysis and notions of continuity in \textsc{Coq}
- 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
- Gappa
- Matita
- Ariadne
- Flocq
- Invariants for the FoCaL language
- Large formal wikis: issues and solutions
- iRRAM
- FoCaL
- AERN
- OpenAxiom
- Coquelicot
- ROSCoq
- Views of pi: definition and computation
- RealCertify
- VeriPhy
- ProofPeer
- Algebraic_VCs
- KAD
- Whelp
- 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
- Formalization of real analysis: a survey of proof assistants and libraries
- Smooth_Manifolds
- 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
