scholarly journals A Unified Type System for Object-Oriented Programming

1990 ◽  
Vol 19 (341) ◽  
Author(s):  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Type System ◽  
Object Oriented ◽  
Type Systems ◽  
Object Oriented Programming ◽  
Type Checking ◽  
Separate Compilation ◽  
Set Inclusion ◽  
New Type ◽  
Efficient Type ◽  
Object Oriented Languages

We present a new type system for object-oriented languages with assignments. Types are sets of classes, subtyping is set inclusion, and genericity is class substitution. The type system enables separate compilation, and unifies, generalizes, and simplifies the type systems underlying SIMULA/BETA, C++, EIFFEL, and Typed Smalltalk, and the type system with type substitutions proposed by Palsberg and Schwartzbach, Classes and types are both modeled as node-labeled, ordered regular trees; this allows an efficient type-checking algorithm.

scholarly journals Substitution Polymorphism for Object-Oriented Programming

1990 ◽  
Vol 19 (305) ◽  
Author(s):  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Type System ◽  
Object Oriented ◽  
Object Oriented Programming ◽  
The Novel ◽  
Type Checking ◽  
Generic Class ◽  
Object Oriented Languages

We introduce substitution polymorphism as a new basis for typed object-oriented languages. While avoiding subtypes and polymorphic types, this mechanism enables optimal static type-checking of generic classes and polymorphic functions. The novel idea is to view a class as having a family of implicit subclasses, each of which is obtained through a substitution of types. This allows instantiation of a generic class to be merely subclassing and resolves the problems in the <em> Eiffel</em> type system reported by Cook. All subclasses, including the implicit ones, can reuse the code implementing their superclass.

A paradigmatic object-oriented programming language: Design, static typing and semantics

1994 ◽  
Vol 4 (2) ◽  
pp. 127-206 ◽  
Author(s):  
Kim B. Bruce
Keyword(s):  
Fixed Points ◽  
Programming Languages ◽  
Programming Language ◽  
Type System ◽  
Object Oriented ◽  
Object Oriented Programming ◽  
Language Design ◽  
Type Checking ◽  
Basic Features ◽  
Oriented Programming Language

AbstractTo illuminate the fundamental concepts involved in object-oriented programming languages, we describe the design of TOOPL, a paradigmatic, statically-typed, functional, object-oriented programming language which supports classes, objects, methods, hidden instance variables, subtypes and inheritance.It has proven to be quite difficult to design such a language which has a secure type system. A particular problem with statically type checking object-oriented languages is designing typechecking rules which ensure that methods provided in a superclass will continue to be type correct when inherited in a subclass. The type-checking rules for TOOPL have this feature, enabling library suppliers to provide only the interfaces of classes with actual executable code, while still allowing users to safely create subclasses. To achieve greater expressibility while retaining type-safety, we choose to separate the inheritance and subtyping hierarchy in the language.The design of TOOPL has been guided by an analysis of the semantics of the language, which is given in terms of a model of the F-bounded second-order lambda calculus with fixed points at both the element and type level. This semantics supports the language design by providing a means to prove that the type-checking rules are sound, thus guaranteeing that the language is type-safe.While the semantics of our language is rather complex, involving fixed points at both the element and type level, we believe that this reflects the inherent complexity of the basic features of object-oriented programming languages. Particularly complex features include the implicit recursion inherent in the use of the keyword, self, to refer to the current object, and its corresponding type, MyType. The notions of subclass and inheritance introduce the greatest semantic complexities, whereas the notion of subtype is more straightforward to deal with. Our semantic investigations lead us to recommend caution in the use of inheritance, since small changes to method definitions in subclasses can result in major changes to the meanings of the other methods of the class.

scholarly journals Strong typing of object-oriented languages revisited

1990 ◽  
Vol 19 (326) ◽  
Author(s):  
Ole Lehrmann Madsen ◽  
Boris Magnusson ◽  
Birger Møller-Pedersen
Keyword(s):  
Programming Language ◽  
Type System ◽  
Object Oriented ◽  
Language Design ◽  
Type Checking ◽  
Programming Language Design ◽  
Dynamic Type ◽  
Language Construct ◽  
Object Oriented Languages

This paper is concerned with the relation between <em>subtyping</em> and <em>subclassing</em> and their influence on programming language design. Traditionally subclassing as introduced by Simula has also been used for defining a hierarchical type system. The type system of a language can be characterized as <em>strong</em> or <em> weak</em> and the type checking mechanism as <em>static</em> or <em>dynamic</em>. Parameterized classes in combination with a hierarchical type-system is an example of a language construct that is known to create complicated type checking situations. In this paper these situations are analyzed and several different solutions are found. It is argued that an approach with a combination of static and dynamic type checking gives a reasonable balance also here. It is also concluded that this approach makes it possible to base the type system on the class/subclass mechanism.

scholarly journals Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny

10.29007/5zjp ◽  
2018 ◽  
Author(s):  
Sylvia Grewe ◽  
Sebastian Erdweg ◽  
Mira Mezini
Keyword(s):  
Formal Methods ◽  
Programming Language ◽  
Type System ◽  
Type Systems ◽  
Domain Specific Languages ◽  
Smt Solver ◽  
Domain Specific ◽  
Efficient Type

\noindent Developing provably sound type systems is a non-trivial task which, as of today, typically requires expert skills in formal methods and a considerable amount of time. Our Veritas~\cite{GreweErdwegWittmannMezini15} project aims at providing support for the development of soundness proofs of type systems and efficient type checker implementations from specifications of type systems. To this end, we investigate how to best automate typical steps within type soundness proofs.\noindent In this paper, we focus on progress proofs for type systems of domain-specific languages. As a running example for such a type system, we model a subset SQL and augment it with a type system. We compare two different approaches for automating proof steps of the progress proofs for this type system against each other: firstly, our own tool Veritas, which translates proof goals and specifications automatically to TPTP~\cite{Sutcliffe98} and calls Vampire~\cite{KovacsV13} on them, and secondly, the programming language Dafny~\cite{Leino2010}, which translates proof goals and specifications to the intermediate verification language Boogie 2~\cite{Leino2008} and calls the SMT solver Z3~\cite{DeMoura2008} on them. We find that Vampire and Dafny are equally well-suited for automatically proving simple steps within progress proofs.

Lightweight family polymorphism

2008 ◽  
Vol 18 (3) ◽  
pp. 285-331 ◽  
Author(s):  
CHIERI SAITO ◽  
ATSUSHI IGARASHI ◽  
MIRKO VIROLI
Keyword(s):  
Type System ◽  
Object Oriented ◽  
Expressive Power ◽  
Type Inference ◽  
Design Decision ◽  
Dependent Types ◽  
Parametric Methods ◽  
Complex Type ◽  
Original Proposal ◽  
Object Oriented Languages

AbstractFamily polymorphism has been proposed for object-oriented languages as a solution to supporting reusable yet type-safe mutually recursive classes. A key idea of family polymorphism is the notion of families, which are used to group mutually recursive classes. In the original proposal, due to the design decision that families are represented by objects, dependent types had to be introduced, resulting in a rather complex type system. In this article, we propose a simpler solution oflightweightfamily polymorphism, based on the idea that families are represented by classes rather than by objects. This change makes the type system significantly simpler without losing much expressive power of the language. Moreover, “family-polymorphic” methods now take a form of parametric methods; thus, it is easy to apply method type argument inference as in Java 5.0. To rigorously show that our approach is safe, we formalize the set of language features on top of Featherweight Java and prove that the type system is sound. An algorithm for type inference for family-polymorphic method invocations is also formalized and proved to be correct. Finally, a formal translation by erasure to Featherweight Java is presented; it is proved to preserve typing and execution results, showing that our new language features can be implemented in Java by simply extending the compiler.

Operations on records

1991 ◽  
Vol 1 (1) ◽  
pp. 3-48 ◽  
Author(s):  
Luca Cardelli ◽  
John C. Mitchell
Keyword(s):  
Type System ◽  
Lambda Calculus ◽  
Object Oriented ◽  
Order Type ◽  
Second Order ◽  
Typed Lambda Calculus ◽  
Semantic Models ◽  
Object Oriented Languages

We define a simple collection of operations for creating and manipulating record structures, where records are intended as finite associations of values to labels. A second-order type system over these operations supports both subtyping and polymorphism. We provide typechecking algorithms and limited semantic models.Our approach unifies and extends previous notions of records, bounded quantification, record extension, and parametrization by row-variables. The general aim is to provide foundations for concepts found in object-oriented languages, within a framework based on typed lambda-calculus.

scholarly journals Static Typing for Object-Oriented Programming

1991 ◽  
Vol 20 (355) ◽  
Author(s):  
Jens Palsberg ◽  
Michael I. Schwartzbach
Keyword(s):  
Partial Order ◽  
Object Oriented ◽  
Object Oriented Programming ◽  
Finite Sets ◽  
Object Oriented Languages ◽  
Static Typing

We develop a theory of statically typed object-oriented languages. It represents classes as labeled, regular trees, types as finite sets of classes, and subclassing as a partial order on trees. We show that our subclassing order strictly generalizes inheritance, and that a novel genericity mechanism arises as an order-theoretic complement. This mechanism, called class substitution, is pragmatically useful and can be implemented efficiently.

Sign in / Sign up

Export Citation Format

Share Document