Sciweavers

MKM
2007
Springer

Formal Representation of Mathematics in a Dependently Typed Set Theory

14 years 5 months ago
Formal Representation of Mathematics in a Dependently Typed Set Theory
Abstract. We have formalized material from an introductory real analysis textbook in the proof assistant Scunak. Scunak is a system based on set theory encoded in a dependent type theory. We use the formalized material to illustrate some interesting aspects of the relationship between informal presentations of mathematics and their formal representation. We focus especially on a representative example proved using the system.
Feryal Fulya Horozal, Chad E. Brown
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where MKM
Authors Feryal Fulya Horozal, Chad E. Brown
Comments (0)