Canonical Big Operators

DOI10.1007/978-3-540-71067-7_11MaRDI QIDQ3543652zbMATH OpenOpenAlexFDO

Authors Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Paşca

Publication date 4 December 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71067-7_11

Mathematics Subject Classification ID

Recommendations

• Coquelicot: a user-friendly library of real analysis for Coq
• Flexary operators for formalized mathematics
• A constructive algebraic hierarchy in Coq.
• scientific article; zbMATH DE number 1070623
• Packaging Mathematical Structures

Cites work

• A Modular Formalisation of Finite Group Theory
• An introduction to small scale reflection in Coq
• scientific article; zbMATH DE number 1670760 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Organizing numerical theories using axiomatic type classes
• Proof-irrelevance out of excluded-middle and choice in the calculus of constructions
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics

Cited in

(23)

• Formal proofs of rounding error bounds. With application to an automatic positive definiteness check
• Functions-as-constructors higher-order unification: extended pattern unification
• Formalization of Shannon's theorems
• Formally verified certificate checkers for hardest-to-round computation
• Trusting computations: a mechanized proof from partial differential equations to actual program
• A Coq formalization of Lebesgue integration of nonnegative functions
• Completeness and decidability results for CTL in constructive type theory
• A certified reduction strategy for homological image processing
• Computational Complexity Via Finite Types
• Point-free, set-free concrete linear algebra
• Formal proofs for theoretical properties of Newton's method
• Hints in Unification
• Packaging Mathematical Structures
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• Finite Groups Representation Theory with Coq
• Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
• Incidence simplicial matrices formalized in Coq/SSReflect
• Implementing type theory in higher order constraint logic programming
• Flexary operators for formalized mathematics
• A formal proof of the expressiveness of deep learning
• A formal proof of the expressiveness of deep learning
• Measure construction by extension in dependent type theory with application to integration
• Formally-verified round-off error analysis of Runge-Kutta methods

Describes a project that uses

Uses Software

• HOL Light
• Coq

This page was built for publication: Canonical Big Operators

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3543652)