Formalizing mathematics in higher-order
✍
François Puitg; Jean-François Dufourd
📂
Article
📅
2000
🏛
Elsevier Science
🌐
English
⚖ 421 KB
An innovative attempt to develop formal techniques of speciÿcation, proof, and program extraction in geometric modelling is reported through the axiomatization of the mathematical model of the combinatorial maps in the calculus of inductive constructions (CIC), a variety of type theory well suited f