research-article

Static typing with value space-based subtyping

Authors:

Alexander Paar,

Stefan GrunerAuthors Info & Claims

SAICSIT '11: Proceedings of the South African Institute of Computer Scientists and Information Technologists Conference on Knowledge, Innovation and Leadership in a Diverse, Multidisciplinary Environment

Pages 177 - 186

https://doi.org/10.1145/2072221.2072242

Published: 03 October 2011 Publication History

Abstract

Numerous programming and schema languages contain the notion of value types. However, support for value space-based subtyping is spotty. This paper presents a formal type system for atomic value types as an extension of the simply typed lambda calculus with subtyping. In the λ_c-calculus, value types can be derived through the application of value space constraints. Type inference rules can be used to infer transient value space constraints that hold for limited scopes of a program. The type system of the λ_c-calculus is proved to be sound. The λ_c-calculus was fully implemented in Java and C#. The presented approach was successfully validated to subsume XML Schema Definition type construction and to facilitate the integration of XSD data types with the C# programming language.

References

[1]

P. V. Biron and A. Malhotra. XML Schema Part 2: Datatypes Second Edition. Technical report, World Wide Web Consortium (W3C), October 2004. 177, 179

[2]

B. Chin, S. Markstrum, and T. Millstein. Semantic type qualifiers. In 27th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 85--95, New York, NY, USA, June 2005. ACM Press. 182

Digital Library

[3]

B. Chin, S. Markstrum, T. D. Millstein, and J. Palsberg. Inference of user-defined type qualifiers and qualifier rules. In P. Sestoft, editor, 15th European Symposium on Programming (ESOP), volume 3924 of Lecture Notes in Computer Science, pages 264--278, Berlin/Heidelberg, Germany, March 2006. Springer Verlag. 183

Digital Library

[4]

J. S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. In 24th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), volume 37 of ACM SIGPLAN Notices, pages 1--12, New York, NY, USA, June 2002. ACM Press. 182

Digital Library

[5]

D. Greenfieldboyce and J. S. Foster. Type qualifier inference for Java. In 22nd ACM SIGPLAN Conference on Object-Oriented Programing, Systems, Languages, and Applications (OOPSLA), volume 42 of ACM SIGPLAN Notices, pages 321--336, New York, NY, USA, October 2007. ACM Press. 183

Digital Library

[6]

HP Labs. Jena Semantic Web Framework, 2004. 182

[7]

Information Society Technology integrated project 506909. Computers in the Human Interaction Loop (CHIL), 2004. 182

[8]

International Organization for Standardization. Representation of dates and times (ISO 8601). Technical report, International Organization for Standardization, December 2004. 178

[9]

G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C. Lopes, J.-M. Loingtier, and J. Irwin. Aspect-oriented programming. In M. Aksit and S. Matsuoka, editors, 11th European Conference on Object-Oriented Programming (ECOOP), volume 1241 of Lecture Notes in Computer Science, pages 220--242. Springer Verlag, June 1997. 182

[10]

R. Lömmel and E. Meijer. Revealing the X/O impedance mismatch (changing lead into gold). In Datatype-Generic Programming, volume 4719 of Lecture Notes in Computer Science, page 80. Springer-Verlag, June 2007. 177, 182

[11]

D. L. McGuinness and F. van Harmelen. OWL Web Ontology Language Overview. Technical report, World Wide Web Consortium (W3C), February 2004. 182

[12]

E. Meijer and W. Schulte. Unifying tables, objects and documents. In Workshop on Declarative Programming in the Context of Object-Oriented Languages (DP-COOL). Forschungszentrum Jülich GmbH, 2003. 177

[13]

Object Management Group. Object Constraint Language, version 2.0. Technical report, Object Management Group, May 2006. 182

[14]

Object Management Group. Unified Modeling Language, infrastructure. Technical report, Object Management Group, February 2009. 182

[15]

Object Management Group. Unified Modeling Language, superstructure. Technical report, Object Management Group, February 2009. 182

[16]

M. Odersky, D. Rabin, and P. Hudak. Call by name, assignment, and the lambda calculus. In 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 43--56, New York, NY, USA, 1993. ACM Press. 181

Digital Library

[17]

A. Paar. Zhi# -- Programming Language Inherent Support for Ontologies. PhD thesis, Universitöt Karlsruhe (TH), Am Fasanengarten 5, 76137 Karlsruhe, Germany, July 2009. 181, 182

[18]

A. Paar, J. Reuter, J. Soldatos, K. Stamatis, and L. Polymenakos. A formally specified ontology management API as a registry for ubiquitous computing systems. Applied Intelligence, 30(1):37--46, February 2009. 182

Digital Library

[19]

B. C. Pierce. Types and Programming Languages. The MIT Press, Cambridge, MA, USA, 2002. 180

Digital Library

[20]

D. Thomas. The impedance imperative: Tuples + objects + infosets = too much stuff! Journal of Object Technology, 2(5):7--12, September-October 2003. 177

Cited By

van der Berg JGruner S(2019)Formal Semantics and Tool Support for a Syntactically Restricted Dialect of SOFLStructured Object-Oriented Formal Language and Method10.1007/978-3-030-13651-2_8(125-145)Online publication date: 9-Feb-2019
https://doi.org/10.1007/978-3-030-13651-2_8

Index Terms

Static typing with value space-based subtyping
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Data types and structures
        Frameworks

Recommendations

Gradual typing with unification-based inference
DLS '08: Proceedings of the 2008 symposium on Dynamic languages

Static and dynamic type systems have well-known strengths and weaknesses. Gradual typing provides the benefits of both in a single language by giving the programmer control over which portions of the program are statically checked based on the presence ...
Typing dynamic typing

Even when programming in a statically typed language we every now and then encounter statically untypable values; such values result from interpreting values or from communicating with the outside world. To cope with this problem most languages include ...
Typing dynamic typing
ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming

Even when programming in a statically typed language we every now and then encounter statically untypable values; such values result from interpreting values or from communicating with the outside world. To cope with this problem most languages include ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

SAICSIT '11: Proceedings of the South African Institute of Computer Scientists and Information Technologists Conference on Knowledge, Innovation and Leadership in a Diverse, Multidisciplinary Environment

October 2011

352 pages

ISBN:9781450308786

DOI:10.1145/2072221

Conference Chair:
Irwin Brown
University of Cape Town
,
Program Chairs:
Kosheek Sewchurran
University of Cape Town
,
Hussein Suleman
University of Cape Town

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

University of Cape Town
SAICSIT: So. African Inst. Of Computer Scientists & Info Tecnologists

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 October 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SAICSIT '11

Sponsor:

SAICSIT

SAICSIT '11: South African Institute of Computer Scientists and Information Technologists Conference

October 3 - 5, 2011

Cape Town, South Africa

Acceptance Rates

Overall Acceptance Rate 187 of 439 submissions, 43%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
76
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

van der Berg JGruner S(2019)Formal Semantics and Tool Support for a Syntactically Restricted Dialect of SOFLStructured Object-Oriented Formal Language and Method10.1007/978-3-030-13651-2_8(125-145)Online publication date: 9-Feb-2019
https://doi.org/10.1007/978-3-030-13651-2_8

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents