Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis

DOI10.1007/978-3-030-51054-1_1MaRDI QIDQ5048989zbMATH OpenOpenAlexFDO

Authors Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi

Publication date 9 November 2022

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-51054-1_1

zbMATH Keywords

Coqdependent type theoryformalization of mathematicspacked classes

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A machine-checked proof of the odd order theorem
• Canonical Big Operators
• Canonical structures for the working Coq user
• Coquelicot: a user-friendly library of real analysis for Coq
• First-Class Type Classes
• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
• Formalization techniques for asymptotic reasoning in classical analysis
• Hints in Unification
• scientific article; zbMATH DE number 3442061 (Why is no real title available?)
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• Packaging Mathematical Structures
• Telescopic mappings in typed lambda calculus
• The Architecture of Mathematics
• The Lean theorem prover (system description)
• Type classes for mathematics in type theory
• Validating Mathematical Structures

Cited in

(10)

• Validating Mathematical Structures
• scientific article; zbMATH DE number 7168151 (Why is no real title available?)
• Measure construction by extension in dependent type theory with application to integration
• Towards a practical library for monadic equational reasoning in Coq
• Multiple-inheritance hazards in dependently-typed algebraic hierarchies
• Graded rings in Lean's dependent type theory
• Algorithm and abstraction in formal mathematics
• Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi (system description)
• A practical formalization of monadic equational reasoning in dependent-type theory
• Use and abuse of instance parameters in the Lean mathematical library.

Describes a project that uses

Uses Software

• Coq
• Agda
• Isabelle
• HoTT
• Nuprl
• Coquelicot
• Lean
• GitHub

This page was built for publication: Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis

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