A Unified Formal Description of Arithmetic and Set Theoretical Data Types

Preprint English OPEN
Tarau, Paul;
(2010)
  • Subject: Computer Science - Symbolic Computation | Computer Science - Logic in Computer Science
    arxiv: Computer Science::Programming Languages | Computer Science::Mathematical Software

We provide a "shared axiomatization" of natural numbers and hereditarily finite sets built around a polymorphic abstraction of bijective base-2 arithmetics. The "axiomatization" is described as a progressive refinement of Haskell type classes with examples of instances ... View more
  • References (10)

    1. Kaye, R., Wong, T.L.: On Interpretations of Arithmetic and Set Theory. Notre Dame J. Formal Logic Volume 48(4) (2007) 497{510

    2. Jones, S.P., Jones, M., Meijer, E.: Type classes: An exploration of the design space. In: Haskell Workshop. (1997)

    3. Pettigrew, R.: On Interpretations of Bounded Arithmetic and Bounded Set Theory Notre Dame J. Formal Logic Volume 50, Number 2 (2009), 141-151.

    4. Tarau, P.: A Groupoid of Isomorphic Data Transformations. In Carette, J., Dixon, L., Coen, C.S., Watt, S.M., eds.: Intelligent Computer Mathematics, 16th Symposium, Calculemus 2009, 8th International Conference MKM 2009 , Grand Bend, Canada, Springer, LNAI 5625 (July 2009) 170{185

    5. Tarau, P.: Isomorphisms, Hylomorphisms and Hereditarily Finite Data Types in Haskell. In: Proceedings of ACM SAC'09, Honolulu, Hawaii, ACM (March 2009) 1898{1903

    6. Tarau, P.: An Embedded Declarative Data Transformation Language. In: Proceedings of 11th International ACM SIGPLAN Symposium PPDP 2009, Coimbra, Portugal, ACM (September 2009) 171{182

    7. Kirby, L.: Addition and multiplication of sets. Math. Log. Q. 53(1) (2007) 52{65

    8. Vuillemin, J.: Digital algebra and circuits. In Dershowitz, N., ed.: Veri cation: Theory and Practice. Volume 2772 of Lecture Notes in Computer Science., Springer (2003) 733{746

    9. Coquand, T., Huet, G.: The calculus of constructions. Information and Computation 76(2/3) (1988) 95{120

    10. The Coq development team: The Coq proof assistant reference manual. LogiCal Project. (2004) Version 8.0.

  • Metrics
Share - Bookmark