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