Canonical Big Operators

DOI10.1007/978-3-540-71067-7_11zbMath1165.68450OpenAlexW1542112699MaRDI QIDQ3543652

Georges Gonthier, Yves Bertot, 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

Related Items (22)

Completeness and decidability results for CTL in constructive type theory ⋮ Functions-as-constructors higher-order unification: extended pattern unification ⋮ Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis ⋮ Hints in Unification ⋮ Packaging Mathematical Structures ⋮ Wave equation numerical resolution: a comprehensive mechanized proof of a C program ⋮ Trusting computations: a mechanized proof from partial differential equations to actual program ⋮ A Certified Reduction Strategy for Homological Image Processing ⋮ Computational Complexity Via Finite Types ⋮ A Coq formalization of Lebesgue integration of nonnegative functions ⋮ Measure construction by extension in dependent type theory with application to integration ⋮ Formally-verified round-off error analysis of Runge-Kutta methods ⋮ Formal proofs of rounding error bounds. With application to an automatic positive definiteness check ⋮ A formal proof of the expressiveness of deep learning ⋮ A formal proof of the expressiveness of deep learning ⋮ Incidence Simplicial Matrices Formalized in Coq/SSReflect ⋮ Point-Free, Set-Free Concrete Linear Algebra ⋮ Finite Groups Representation Theory with Coq ⋮ Formal proofs for theoretical properties of Newton's method ⋮ Implementing type theory in higher order constraint logic programming ⋮ Formalization of Shannon's theorems ⋮ Formally verified certificate checkers for hardest-to-round computation

Uses Software

• HOL Light
• Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• 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
• A Modular Formalisation of Finite Group Theory
• Theorem Proving in Higher Order Logics
• Theorem Proving in Higher Order Logics
• Proof-irrelevance out of excluded-middle and choice in the calculus of constructions

This page was built for publication: Canonical Big Operators