Explicit mathematics: power types and overloading

Annals of Pure and Applied Logic 134 (2-3):284-302 (2005)

Systems of explicit mathematics provide an axiomatic framework for representing programs and proving properties of them. We introduce such a system with a new form of power types using a monotone power type generator. These power types allow us to model impredicative overloading. This is a very general form of type dependent computation which occurs in the study of object-oriented programming languages. We also present a set-theoretic interpretation for monotone power types. Thus establishing the consistency our system of explicit mathematics
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/j.apal.2004.12.002
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 40,066
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

View all 11 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Power Types in Explicit Mathematics?Gerhard Jäger - 1997 - Journal of Symbolic Logic 62 (4):1142-1146.
Uniform Inseparability in Explicit Mathematics.Andrea Cantini & Pierluigi Minari - 1999 - Journal of Symbolic Logic 64 (1):313-326.
On Power Set in Explicit Mathematics.Thomas Glass - 1996 - Journal of Symbolic Logic 61 (2):468-489.
Realisability in Weak Systems of Explicit Mathematics.Daria Spescha & Thomas Strahm - 2011 - Mathematical Logic Quarterly 57 (6):551-565.
Universes in Explicit Mathematics.Gerhard Jäger, Reinhard Kahle & Thomas Studer - 2001 - Annals of Pure and Applied Logic 109 (3):141-162.
Explicit Mathematics with the Monotone Fixed Point Principle.Michael Rathjen - 1998 - Journal of Symbolic Logic 63 (2):509-542.
The NCTM Standards and the Philosophy of Mathematics.Charalampos Toumasis - 1997 - Studies in Philosophy and Education 16 (3):317-330.
Realization of Analysis Into Explicit Mathematics.Sergei Tupailo - 2001 - Journal of Symbolic Logic 66 (4):1848-1864.
What is Special About “Implicit” and “Explicit”?Geir Overskeid - 1999 - Behavioral and Brain Sciences 22 (5):780-780.
Liberty as Power.Preston King - 1999 - Critical Review of International Social and Political Philosophy 2 (3):1-25.


Added to PP index

Total views
4 ( #1,035,882 of 2,236,459 )

Recent downloads (6 months)
4 ( #465,157 of 2,236,459 )

How can I increase my downloads?


Sorry, there are not enough data points to plot this chart.

My notes

Sign in to use this feature