Competing inheritance paths in dependent type theory: a case study in functional analysis

The purpose of this webpage is to provide the formalization accompanying the following paper:

• Competing inheritance paths in dependent type theory: a case study in functional analysis
  • to appear in the proceedings of IJCAR 2020
  • open access: HAL (pdf)
  • slides used at IJCAR 2020

Accompanying material:

• stand-alone distribution of MathComp-Analysis + mockups for forgetful inheritance (tar.gz)
• contents overview:
  • README.txt
  • Makefile
  • mockups/
    • packed_classes.v
    • type_classes.v
    • type_classes.lean
    • scalar_notations/
  • math-comp/
  • bigenough/
  • finmap/
  • analysis/

The last version of MathComp-Analysis:

• on github