Which comes first: the object or the class? Language designers enjoy the conceptual simplicity of object-based languages (such as Emerald or Self) while many programmers prefer the pragmatic utility of classical inheritance (as in Simula and Java). Programmers in object-based languages have a tendency to build libraries to support traditional inheritance, and language implementations are often contorted to the same end. In this paper, we revisit the relationship between classes and objects. We model various kinds of inheritance in the context of an object-oriented language whose objects are not defined by classes, and explain why class inheritance and initialisation cannot be easily modelled purely by delegation.

No abstract available.

Many programming language constructs that support software engineering in the large - explicit variable declarations, explicit external dependencies, static types, information hiding, invariants-provide little benefit to the small programs written by novice programmers, where every extra syntactic token has to be explained and understood before novices can succeed in running even the simplest program. We are designing Grace, a new educational object-oriented language that we hope will prove useful for teaching both programming and software engineering. This paper describes some of the tradeoffs between teaching programming and teaching software engineering that we faced while designing Grace, and our attempts to address those tradeoffs.

Grace is a new object-oriented language that supports a variety of approaches to teaching programming. It integrates accepted new ideas in programming languages into a simple language that allows students and teachers to focus on the essential complexities of programming rather than the accidental complexities of the language. We motivate Grace, review its design, and evaluate it against Kolling's criteria.

Object orientation and pattern matching are often seen as conflicting approaches to program design. Object-oriented programs place type-dependent behavior inside objects and invoke it via dynamic dispatch, while pattern-matching programs place type-dependent behavior outside data structures and invoke it via multiway conditionals (case statements).

Because of the growing importance of concurrent programming, many people are trying to figure out where in the curriculum to introduce students to concurrency. In this paper we discuss the use of concurrency in an introductory computer science course. This course, which has been taught for ten years, introduces concurrency in the context of event-driven programming. It also makes use of graphics and animations with the support of a library that reduces the syntactic overhead of using these constructs. Students learn to use separate threads in a way that enables them to write programs that match their intuitions of the world. While the separate threads do interact, programs are selected so that race conditions are generally not an issue.

This special session is devoted to identifying the CS education papers of the 20th century that have had the greatest influence on our practice of CS education today. The point is not primarily to produce the list of papers; rather it is to derive criteria, principles, and practices for identifying valuable contributions to CS education. This will provide a basis for establishing of awards or other recognition for influential contributions to CS education; it may also clarify the criteria for reviewing all papers. Invited participants will identify influential papers and their criteria for selecting them; the audience will also be encouraged to nominate papers and propose selection criteria. The results of this session will be communicated to the SIGCSE leadership, who will decide whether, and how, to implement any actual awards.

With the support of a grant from the Sloan Foundation, nine computer scientists from liberal arts colleges came together in October, 1984 to form the Liberal Arts Computer Science Consortium (LACS) and to create a model curriculum appropriate for liberal arts colleges. Over the years the membership has grown and changed, but the focus has remained on helping to establish and maintain high-quality computer science programs in liberal arts colleges. In this report we discuss briefly the history of the group, the series of three curricula produced by LACS, and other contributions of the members to computer science education.

This special session will present a summary of the recommendations of the First SIGPLAN Workshop on Undergraduate Programming Language Curricula, held at Harvard University in May, 2008. The purpose of the workshop was to generate new recommendations for programming languages topics to be learned by all undergraduate CS majors. In this special session we will present a summary of the curriculum recommendations, why they were made, and ways of incorporating them into undergraduate CS curricula.

The participants will use a debate format with a provocative thesis to explore the pedagogical approach known as "objects early" or "objects first." By arguing in the affirmative, Elliot Koffman and Stuart Reges will point out concerns that have been raised about the approach. By arguing in the negative, Kim Bruce and Michael Kölling will describe schools that are succeeding with the approach and ways to address significant concerns. Owen Astrachan as moderator will ensure that the debate remains civil and will provide some humorous and possibly even insightful commentary on the evidence presented by both sides.

Various software tools have been proposed or developed for use in introductory programming courses. Usually, presentation of a new tool at the SIGCSE symposium occurs when a tool is first developed, leaving it to interested observers to identify success or failure of tools over their lifetime.For teachers, it can be difficult to compare available tools and judge potential application in their courses.In this session, three tools with an established track record of successful classroom use are presented: Karel J Robot [1], objectdraw [2], and BlueJ [2]. In addition to considering each tool individually, opportunities for combinations of these tools are also discussed.The focus of this session will be on concrete, hands-on advice that teachers can immediately apply in their classrooms.

As instructors we work hard at teaching our students why and how to create appropriate abstractions in order to simplify program design and implementation. Interestingly, we sometimes neglect to take advantage of the fact that we can also use abstractions to benefit teaching and learning. In this talk I'll present some examples of useful abstractions that can make computer science concepts more concrete for novices. I'll also discuss the importance of understanding and using languages that provide support for creating abstractions in developing software.

The approach to teaching recursion in introductory programming courses has changed little during the transition from procedural to object-oriented languages. It is still common to present recursion late in the course and to focus on traditional, procedural examples such as calculating factorials or solving the Towers of Hanoi puzzle. In this paper, we propose that the shift to object-oriented programming techniques calls for a significant shift in our approach to teaching recursion. First, we argue that in the context of object-oriented programming students should be introduced to examples of simple recursive structures such as linked lists and methods that process them, before being introduced to traditional procedural examples. Second, we believe that this material should be presented before students are introduced to structures such as arrays. In our experience, the early presentation of recursive structures provides the opportunity to reinforce the fundamentals of defining and using classes and better prepares students to appreciate the reasons to use classes to encapsulate access to other data structures when they are presented.

SIGCSE 2004 marked the official announcement of the ACM Java Task Force, which is working to develop a stable collection of pedagogical resources that will make it easier to teach Java to first-year computing students. The Java Task Force has received funding from the ACM Education Board, the SIGCSE Special Projects Fund, and the National Science Foundation (NSF Award DUE-0411905). This session offers an update on the work of the Java Task Force over the past year and provides an opportunity for community feedback prior to the publication of the final report in June 2005.

No abstract available.

PolyTOIL is a new statically typed polymorphic object-oriented programming language that is provably typesafe. By separating the definitions of subtyping and inheritance, providing a name for the type of self, and carefully defining the type-checking rules, we have obtained a language that is very expressive while supporting modular type-checking of classes. Thematchingrelation on types, which is related to F-bounded quantification, is used both in stating type-checking rules and expressing the bounds on type parameters for polymorphism. The design of PolyTOIL is based on a careful formal definition of type-checking rules and semantics. A proof of type safety is obtained with the aid of a subject reduction theorem.

We have recently designed a CS 1 course that integrates event-driven programming from the very start. Our experience teaching this course runs counter to the prevailing sense that these techniques would add complexity to the content of CS 1. Instead, we found that they were simple to present and that they also simplified the presentation of other material in the course. In this paper, we explain the approach we used to introduce event-driven methods and discuss the factors underlying our success.

In this paper we describe a library we have developed that supports an "OO-from-the-beginning" approach to CS 1. The use of real graphics "objects" and event-driven programming are important components of our approach. The design of interactive graphical programs helps students to both use objects and write methods early while designing and implementing interesting programs.

The paper [2] argued that mathematical ideas play an important role in the computer science curriculum, and that Discrete Mathematics needs to be taught early in the computer science curriculum. In this follow-up paper, we present evidence that computer science curricula are drifting away from a fundamental commitment to theoretical and mathematical ideas. We propose some actions that can be taken to help reverse this drift.

We are concerned about a view in undergraduate computer science education, especially in the early courses, that it's okay to be math-phobic and still prepare oneself to become a computer scientist. Our view is the contrary: that any serious study of computer science requires students to achieve mathematical maturity (especially in discrete mathematics) early in their undergraduate studies, thus becoming well-prepared to integrate mathematical ideas, notations, and methodologies throughout their study of computer science. A major curricular implication of this theme is that the prerequisite expectations and conceptual level of the first discrete mathematics course should be the same as it is for the first calculus course --- secondary school pre-calculus and trigonometry. Ultimately, calculus, linear algebra, and statistics are also essential for computer science majors, but none should occur earlier than discrete mathematics. This paper explains our concerns and outlines our response as a series of examples and recommendations for future action.

Most junior-senior level programming languages courses approach the subject either from the point-of-view of principles (concepts) of programming languages or from the perspective of understanding languages through writing progressively more complex interpreters. In this paper we show how to use formal semantics in a series of interpreter assignments in a principles or concepts-based course. The interpreter assignments make the semantics more concrete for students while providing a deeper understanding of concepts.

No abstract available.

This paper addresses the design of an exciting introductory course for entering college students who have some programming background.The key innovation of the course is the introduction of material pertaining to experimental graph reduction and dataflow archltectures for highly-parallel computers.The success of the course is attributed to interesting, well-integrated material and the use of visually-oriented interactive simulators for the architectures.

Abstract To 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.

Over the last several years, much interesting work has been done in modelling object-oriented programming languages in terms of extensions of the bounded second-order lambda calculus, F . Unfortunately, it has recently been shown by Pierce ([Pie92]) that type checking F is undecidable. Moreover, he showed that the undecidability arises in the seemingly simpler problem of determining whether one type is a subtype of another. In [Bru93a, Bru93b], the first author introduced a statically-typed, functional, object-oriented programming language, TOOPL, which supports classes, objects, methods, instance variables, subtypes, and inheritance. The semantics of TOOPL is based on F , so the question arises whether type checking in this language is decidable. In this paper we show that type checking for TOOPLE, a minor variant of TOOPL (Typed Object-Oriented Programming Language), is decidable. The proof proceeds by showing that subtyping is decidable, that all terms of TOOPLE have minimum types...

In this paper we introduce a statically-typed, functional, object-oriented programming language, TOOPL, which supports classes, objects, methods, instance variable, subtypes, and inheritance.

A constructive characterization is given of the isomorphisms which must hold in all models of the typed lambda calculus with surjective pairing. Using the close relation between closed Cartesian categories and models of these calculi, we also produce a characterization of those isomorphisms which hold in all CCC's. Using the correspondence between these calculi and proofs in intuitionistic positive propositional logic, we thus provide a characterization of equivalent formulae of this logic, where the definition of equivalence of terms depends on having “invertible” proofs between the two terms. Work of Rittri (1989), on types as search keys in program libraries, provides an interesting example of use of these characterizations.

The authors give a formal semantics for the language Bounded Fun, which supports both parametric and subtype polymorphism. They show how to use partial equivalence relations to model inheritance in this language, which supports the notion of subtype and record types. A generalization of partial equivalence relations, known as omega -sets, is used in combination with modest sets to provide the first known model of Bounded Fun (with explicit polymorphism). Connections with previous work on the semantics of explicit parametric polymorphism is established by noting that the semantics of polymorphic types presented here (using dependent products) is isomorphic to that given by the intersection interpretation of polymorphism.>

Manypeople feel that recent ACM statements on computing do not match well with the traditions and standards of most liberal arts colleges.During the Fall of 1984, representatives from nine liberal arts colleges participated in a workshop sponsored by the Alfred P. Sloan Foundation which was aimed at developing an undergraduate computer science concentration suitable for liberal arts colleges.

Article Free Access Share on Provable isomorphisms and domain equations in models of typed languages Authors: K B Bruce Department of Mathematical Sciences, Williams College, Williamstown, Ma. Department of Mathematical Sciences, Williams College, Williamstown, Ma.View Profile , G Longo Dipartimento di Informatica, Universita di Pisa, Pisa, Italy Dipartimento di Informatica, Universita di Pisa, Pisa, ItalyView Profile Authors Info & Claims STOC '85: Proceedings of the seventeenth annual ACM symposium on Theory of computingDecember 1985 Pages 263–272https://doi.org/10.1145/22145.22175Published:01 December 1985Publication History 31citation248DownloadsMetricsTotal Citations31Total Downloads248Last 12 Months21Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

In this series of two papers we wish to discuss two new methods of constructing models for an arbitrary theory T of stationary logic, L(aa). The original work in constructing models for this logic appears in Barwise-Kaufmann-Makkai [BKM] (which we shall refer to as BKM for brevity). In that paper the authors prove completeness, compactness, and omitting types theorems for L(aa) by a technique similar to that used by Keisler [1970] in constructing models of L(Q1), logic with the generalized quantifier “there exist uncountably many”. In this paper we give an alternative method of constructing models using a method of model-theoretic forcing similar to that of Bruce [1978]. In a succeeding paper we will give yet another method of constructing models using definable ultrapowers. As applications of this new forcing construction we give new proofs of the completeness and omitting types theorems for LB(aa), where LB(aa) is any countable fragment of Lω1ω(aa). We also give new proofs of versions of the Barwise completeness and compactness theorems for LA(aa) where A is a countable admissible set. In proofs of these theorems the model constructions via forcing are used in a way very similar to that of consistency properties in Lω1ω. Aside from the ease in handling the model theory of Lω1ω(aa) we see two other advantages in this sort of model construction. The first is in the ability to prove versions of theorems relativized to formulas of low complexity (e.g. relativized omitting types theorems). The second is that we have a high degree of control over the construction of standard models and hence have a better knowledge of the structure of the model (see the remarks following the proof of Lemma 3.3), something that should prove useful in constructing more complicated models.

Abstract The language LA(Ⅎ) is formed by adding the quantifier Ⅎx, “few x”, to the infinitary logic LA on an admissible set A. A complete axiomatization is obtained for models whose universe is the set of ordinals of A and where Ⅎx is interpreted as there exist A-finitely many x. For well-behaved A, every consistent sentence has a model with an A-recursive diagram. A principal tool is forcing for LA(Ⅎ).

It is the purpose of this paper to investigate the model theory of logic with a generalized quantifier; in particular the logic L(Q1) where Q1xφ(x) has the intended meaning “there exist uncountably many x such that φ(x)”. We do this from the point of view that the best way to study what happens in the so-called “ω1-standard” models of L(Q1) is to examine the countable ideal models of L(Q) that satisfy all of the axioms for L(Q1) (see definitions of ω1-standard and ideal models in §1). We believe that this study can be as fruitful for L(Q1) as the study of countable models of ZF has been for set theory. A major problem is formulating an adequate definition of submodel for countable ideal models that is compatible with that for ω1-standard models. Thus we begin the paper by discussing several possible definitions of the notion of submodel. We then adopt a particular definition of submodel and investigate model-completeness in L(Q). We define model-completeness both for ω1-standard models and for countable ideal models and compare the two notions. We also examine elimination of quantifiers, as well as investigating formulas preserved under submodels, again both for ω1-standar d and countable ideal models.