Mathematical Knowledge Management
From MaRDI portal
Publication:5313080
DOI10.1007/b100478zbMath1108.68586OpenAlexW4234388457MaRDI QIDQ5313080
Herman Geuvers, Luís Cruz-Filipe, Freek Wiedijk
Publication date: 26 August 2005
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/b100478
Related Items
Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ Invariants for the FoCaL language ⋮ Axiomatic reals and certified efficient exact real computation ⋮ Formal Verification of Exact Computations Using Newton’s Method ⋮ Unnamed Item ⋮ Working with Mathematical Structures in Type Theory ⋮ Combining higher-order logic with set theory formalizations ⋮ Unnamed Item ⋮ Certified Exact Transcendental Real Number Computation in Coq ⋮ Quantitative continuity and Computable Analysis in Coq ⋮ User interaction with the Matita proof assistant ⋮ Coquelicot: a user-friendly library of real analysis for Coq ⋮ A computer-verified monadic functional implementation of the integral ⋮ C-CoRN ⋮ Continuous and monotone machines ⋮ A Formal Proof of Cauchy’s Residue Theorem ⋮ Proof assistants: history, ideas and future ⋮ Automating Side Conditions in Formalized Partial Functions ⋮ Constructive hybrid games ⋮ Web Interfaces for Proof Assistants
Uses Software