The following pages link to C-CoRN (Q18827):
Displaying 39 items.
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL (Q832721) (← links)
- A computer-verified monadic functional implementation of the integral (Q987984) (← links)
- Proof assistants: history, ideas and future (Q1040001) (← links)
- Coquelicot: a user-friendly library of real analysis for Coq (Q2018661) (← links)
- Constructive hybrid games (Q2096468) (← links)
- Axiomatic reals and certified efficient exact real computation (Q2148797) (← links)
- Invariants for the FoCaL language (Q2379680) (← links)
- User interaction with the Matita proof assistant (Q2462635) (← links)
- A Formal Proof of Cauchy’s Residue Theorem (Q2829261) (← links)
- Web interfaces for proof assistants (Q2867935) (← links)
- Formalization of real analysis: a survey of proof assistants and libraries (Q2973239) (← links)
- Formal proofs for theoretical properties of Newton's method (Q3094171) (← links)
- A formal study of Bernstein coefficients and polynomials (Q3094174) (← links)
- Type classes for mathematics in type theory (Q3094177) (← links)
- Formal Verification of Exact Computations Using Newton’s Method (Q3183542) (← links)
- Constructive analysis, types and exact real numbers (Q3431542) (← links)
- Affine functions and series with co-inductive real numbers (Q3431543) (← links)
- (Q3497625) (← links)
- Working with Mathematical Structures in Type Theory (Q3499757) (← links)
- Certified Exact Transcendental Real Number Computation in Coq (Q3543662) (← links)
- A Wiki for Mizar: Motivation, Considerations, and Initial Prototype (Q3582731) (← links)
- Finite Groups Representation Theory with Coq (Q3637300) (← links)
- Type classes for efficient exact real arithmetic in Coq (Q4913763) (← links)
- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives (Q4916067) (← links)
- (Q4989411) (← links)
- (Q5015189) (← links)
- Views of Pi: definition and computation (Q5195256) (← links)
- Large Formal Wikis: Issues and Solutions (Q5200113) (← links)
- Mathematical Knowledge Management (Q5313053) (← links)
- Mathematical Knowledge Management (Q5313079) (← links)
- Mathematical Knowledge Management (Q5313083) (← links)
- The Picard Algorithm for Ordinary Differential Equations in Coq (Q5327365) (← links)
- Automating Side Conditions in Formalized Partial Functions (Q5505512) (← links)
- Automated Machine-Checked Hybrid System Safety Proofs (Q5747654) (← links)
- Developing the Algebraic Hierarchy with Type Classes in Coq (Q5747673) (← links)
- Quantitative continuity and Computable Analysis in Coq (Q5875440) (← links)
- Types for Proofs and Programs (Q5898170) (← links)
- Mathematical Knowledge Management (Q5898518) (← links)
- Mathematical Knowledge Management (Q5898528) (← links)
