, Proceedings, vol.564, pp.163-179, 2013.
On algebraic hierarchies 566 in mathematical repository of Mizar, 2016 Federated Conference on Computer Science and 567 Information Systems (FedCSIS), pp.363-371, 2016. ,
Type classes and filters for mathematical 569 analysis in Isabelle/HOL, Interactive Theorem Proving -4th International Conference, 570 ITP 2013, pp.279-294, 2013. ,
Canonical structures for the working coq user, p.573 ,
URL : https://hal.archives-ouvertes.fr/hal-00816703
, Theorem Proving -4th International Conference, ITP 2013, 2013.
, Proceedings, pp.19-34, 2013.
, The Lean mathematical library, Proceedings of the 9th ACM 576 SIGPLAN International Conference on Certified Programs and Proofs, vol.2020, pp.367-381, 2020.
Programming with Higher-Order Logic, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00776197
Higher-order abstract syntax, Proceedings of the 582 ,
, Conference on Programming Language Design and Implementation, p.583, 1988.
, PLDI '88, vol.584, pp.199-208, 1988.
Dependently typed records in type theory, Formal Aspects of Computing, vol.586, pp.386-402, 2002. ,
A scalable module system. Information and Com-588 putation, vol.230, pp.1-54, 2013. ,
Formalisation Tools for Classical Analysis -A Case Study in Control Theory ,
URL : https://hal.archives-ouvertes.fr/tel-02333396
Typing algorithm in type theory with inheritance, 24th ACM SIGPLAN-593 SIGACT Symposium on Principles of Programming Languages, vol.594, pp.292-301, 1997. ,
Outils Génériques de Modélisation et de Démonstration pour la Formalisation 596 ,
, des Mathématiques en Théorie des Types. Application à la Théorie des Catégories. (Formal-597 ization of Mathematics in Type Theory. Generic tools of Modelisation and Demonstration
, Application to Category Theory), vol.599, 1999.
Validating mathematical structures, accepted in the proceedings of 601 IJCAR 2020, 2020. ,
Type classes for mathematics in type theory ,
, Structures in Computer Science, vol.21, issue.4, pp.795-825, 2011.
, Coq plugin embedding Elpi, vol.605
, Context (A : Type) (f : Ring_of_AbelianGroup A), HB.builders
, Fact mul0r : left_zero zero mul
, 65 move=> x; rewrite -[LHS]add0r addrC. 66 rewrite -{2}(addNr (mul x x)) (addrC (opp _)) addrA
, Fact mulr0 : right_zero zero mul