arXiv subjects

Moez A. AbdelGawad

Publications and source records attributed to Moez A. AbdelGawad.

23 records · Page 2Linked to original sources

arXiv2017

Towards a Java Subtyping Operad

The subtyping relation in Java exhibits self-similarity. The self-similarity in Java subtyping is interesting and intricate due to the existence of wildcard types and, accordingly, the existence of three subtyping rules for generic types: covariant subtyping, contravariant subtyping and invariant subtyping. Supporting bounded type variables also adds to the complexity of the subtyping relation in Java and in other generic nominally-typed OO languages such as C# and Scala. In this paper we explore defining an operad to model the construction of the subtyping relation in Java and in similar generic nominally-typed OO programming languages. Operads, from category theory, are frequently used to model self-similar phenomena. The Java subtyping operad, we hope, will shed more light on understanding the type systems of generic nominally-typed OO languages.

cs.PL↗

arXiv2017

Novel Uses of Category Theory in Modeling OOP

An outline and summary of four new potential applications of category theory to OOP research are presented. These include (1) the use of operads to model Java subtyping, (2) the use of Yoneda's lemma and representable functors in the modeling of generic types in generic nominally-typed OOP, (3) using a combination of category presentations and cartesian closed categories to model structurally-typed OOP, and (4) the use of adjoint functors to model Java erasure.

cs.PL↗

arXiv2016

Towards an Accurate Mathematical Model of Generic Nominally-Typed OOP

The construction of GNOOP as a domain-theoretic model of generic nominally-typed OOP is currently underway. This extended abstract presents the concepts of `nominal intervals' and `full generication' that are likely to help in building GNOOP as an accurate mathematical model of generic nominally-typed OOP. The abstract also presents few related category-theoretic suggestions. The presented concepts and suggestions are particularly geared towards enabling GNOOP to offer a precise and simple view of so-far-hard-to-analyze features of generic OOP such as variance annotations (e.g., Java wildcard types) and erased generics (e.g., Java type erasure).

cs.PL↗

arXiv2015

Set Theory for The (Smart) Masses

Proof Designer is a computer software program designed to help Mathematics students learn to write mathematical proofs. Under the guidance of the user, Proof Designer assists in writing outlines of proofs in elementary set theory. Proof Designer was designed by Daniel Velleman in association with his book "How To Prove It: A Structured Approach" to help students apply the methods discussed in the book, making classes based on the book more interactive. This article is an early report on the progress of our effort to "bring set theory to the masses" by developing Proof Maker, a new Proof Designer-inspired software that ports Proof Designer to hand-held devices such as smart-phones and tablets. Proof Maker, when completed, will allow students to use Proof Designer with the ease of a touch, literally, on their smart devices. Our goal behind developing Proof Maker is to enable any one who is interested enough to develop elementary set theory proofs anywhere he or she might be (think of doing proofs while waiting at a bus stop!) and at any time he or she wishes (think of writing proofs before going to bed, or even in bed!). In this paper we report on the improvements we made to Proof Designer so far, and on the (many) steps remaining for us to have a fully-functioning Proof Maker "in our hands".

math.HO↗

arXiv2014

Domain Theory for Modeling OOP: A Summary

Domain theory is `a mathematical theory that serves as a foundation for the semantics of programming languages'. Domains form the basis of a theory of partial information, which extends the familiar notion of partial function to encompass a whole spectrum of "degrees of definedness", so as to model incremental higher-order computation (i.e., computing with infinite data values, such as functions defined over an infinite domain like the domain of integers, infinite trees, and such as objects of object-oriented programming). General considerations from recursion theory dictate that partial functions are unavoidable in any discussion of computability. Domain theory provides an appropriately abstract setting in which the notion of a partial function can be lifted and used to give meaning to higher types, recursive types, etc. NOOP is a domain-theoretic model of nominally-typed OOP. NOOP was used to prove the identification of inheritance and subtyping in mainstream nominally-typed OO programming languages and the validity of this identification. In this report we first present the definitions of basic domain theoretic notions and domain constructors used in the construction of NOOP, then we present the construction of a simple structural model of OOP called COOP as a step towards the construction of NOOP. Like the construction of NOOP, the construction of COOP uses earlier presented domain constructors.

cs.PL↗