# Links to Kim Bruce's recent papers and talks

This file contains titles and abstracts of papers which can be found in ".dvi" and ".ps" form in this directory. They are broken into Research and Teaching and are listed in each category with the most recent first. Most of the papers available on this site were developed with the support of a series of NSF Research and Educational grants.

Theses of my most recent honors students are also available on-line.

Slides from some recent public lectures that I have given are also available.

Papers are available in the general categories of Research and Teaching / Education.

## RECENT TALKS

• Teaching with Grace. Video of invited talk at Lang.Next 2012 in April, 2012.

• Object-Oriented Languages, Fixed Points, and Systems of Objects, invited talk at FOOL 2005: FOOL05.pdf

• Using Abstractions to Make Concepts Concrete, keynote lecture at SIGCSE 2005.

• ## RESEARCH

Seeking Grace: A new object-oriented language for novices Andrew P. Black, Kim B. Bruce, Michael Homer, James Noble, Amy Ruskin, and Richard Yannow. Proceedings of SIGCSE Computer Science Education 2013. ACM, New York, NY, USA, 2013, pp. 129-134.

Patterns as objects in grace. Michael Homer, James Noble, Kim B. Bruce, Andrew P. Black, and David J. Pearce. Proceedings of the 8th symposium on Dynamic languages (DLS '12). ACM, New York, NY, USA, 2012, pp. 17-28.

Grace: the Absence of (Inessential) Difficulty. Andrew P. Black, Kim B. Bruce, Michael Homer, and James Noble Proceedings of the ACM international symposium on New ideas, new paradigms, and reflections on programming and software (Onward! '12). ACM, New York, NY, USA, 2012, pp. 85-98.

A history of the Liberal Arts Computer Science Consortium and its model curricula by Kim B. Bruce, Robert Cupper, and Scot Drysdale
Transactions on Computing Education, 10 (2010), pp. 1--12.

• On reacting to assertions and polar questions by Donka Farkas and Kim B. Bruce
Journal of Semantics 27 (2010), pp. 81 -- 118.

• LOOJ: Weaving LOOM into Java by Kim B. Bruce and J. Nathan Foster
Proceedings of ECOOP 2004. LNCS3086, Springer-Verlag, pp. 390-414, 2004.

• Some Challenging Typing Issues in Object-Oriented Languages, by Kim B. Bruce
Extended abstract. Last revised 6/03.

• Semantics-Driven Language Design: Statically type-safe virtual types in object-oriented languages
by Kim B. Bruce and Joseph Vanderwaart
Extended abstract. Last revised 2/25/99.

• Modules in LOOM: Classes are not enough
by Kim B. Bruce, Leaf Petersen, and Joseph Vanderwaart
Extended abstract. Last revised 4/13/98.

• A statically safe alternative to virtual types
by Kim B. Bruce, Martin Odersky, and Philip Wadler
Extended abstract to be presented at ECOOP98. Last revised 4/1/98.

• Increasing Java's expressiveness with ThisType and match-bounded polymorphism
by Kim B. Bruce
Draft. Last revised 7/5/97.

• Safe static type checking with systems of mutually recursive classes and inheritance
by Kim B. Bruce
Draft. Last revised 9/15/97.

• Comparing Object Encodings,
by Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce.
Information and Computation 155(1999), pp 108-133, an extended abstract appeared in Proceedings of TACS '97, LNCS 1281, Springer-Verlag, pp. 415-438. Last revised 5/6/98.

• Subtyping is not a good Match'' for object-oriented languages,
by Kim B. Bruce, Adrian Fiech, and Leaf Petersen.
Extended abstract appeared in ECOOP '97 Proceedings, LNCS 1241, Springer-Verlag, pp. 104-127. Last revised 3/20/97.

• Typing in object-oriented languages: Achieving expressiveness and safety,
by Kim B. Bruce.
Last revised 9/10/96.

• PolyTOIL: A type-safe polymorphic object-oriented language,
by Kim B. Bruce, Adrian Fiech, Angela Schuett, and Robert van Gent.
An extended abstract appeared in ECOOP '95 Proceedings, LNCS 952, Springer-Verlag, pp. 27-51. The final version appears in ACM TOPLAS, Vol. 25, No 2, March 2003, pp. 225-290.

• On binary methods,
by Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, The Hopkins Objects Group, Gary T. Leavens, and Benjamin Pierce.
Theory and Practice of Object Systems, 1(1995), pp. 221-242. Last revised 12/7/95.

• TOIL: A new Type-safe Object-oriented Imperative Language,
by Kim B. Bruce and Robert van Gent.
Extended abstract. This paper should be considered to be superseded by the PolyTOIL paper above. Last Revised, 10/13/93

• A Paradigmatic Object-Oriented Programming Language: Design, Static Typing and Semantics,
by Kim B. Bruce.
Journal of Functional Programming 4(1994), pp. 127-206.

• Safe and decidable type checking in an object-oriented language,
by Kim B. Bruce, Jon Crabtree, Allyn Dimock, Robert Muller, Thomas P. Murtagh, Robert van Gent.
OOPSLA '93 proceedings, pp. 29-46.

• An operational semantics for TOOPLE: A statically-typed object-oriented programming language,
by Kim B. Bruce, Jonathan Crabtree, and Gerald Kanapathy.
Proceedings of MFPS '93, LNCS 802, Springer-Verlag, 1994, pp. 603-626.

• Safe Type Checking in a Statically-Typed Object-Oriented Programming Language
by Kim B. Bruce.
Proc ACM Symp. Principles of Programming Languages, 1993, pp. 285-298.

• PER models of subtyping, recursive types and higher-order polymorphism,
by Kim B. Bruce and John Mitchell.
Proceedings of POPL '92, pp. 316-327.

• The Equivalence of Two Semantic Definitions for Inheritance in Object-Oriented Languages,
by Kim B. Bruce.
Proceedings of the MFPS '91 Conference, pp. 102-124.

• Detailed abstracts of all papers follow the listings for TEACHING / EDUCATION.

## TEACHING / EDUCATION

• A 2007 Model Curriculum for a Liberal Arts Degree in Computer Science,
by Liberal Arts Computer Science Consortium.
J. Educ. Resour. Comput. 7, 2 (Jun. 2007)

• Why structural recursion should be taught before arrays in CS 1,
by Kim B. Bruce, Andrea Danyluk, and Thomas Murtagh.
Proceedings of the 2005 ACM Symposium on Computer Science Education, pp. 246-250, 2005.

• Controversy on How to Teach CS 1: A discussion on the SIGCSE-members mailing list
by Kim B. Bruce.

• Event-driven programming facilitates learning standard programming concepts
by Kim B. Bruce, Andrea Danyluk, and Thomas Murtagh.
proceedings of 2004 OOPSLA Educator's symposium.

• Why Math?
by Kim B. Bruce, Scot Drysdale, Charles Kelemen, and Allen Tucker
CACM, September, 2003 pp. 41-44.

• Our Curriculum Has Become Math-Phobic!
by Kim B. Bruce, Charles Keleman, and Allen Tucker.
SIGCSE 2001 Proceedings, pp. 243-247

• A library to support a graphics based object-first approach to CS 1
by Kim B. Bruce, Andrea Danyluk, and Thomas Murtagh.
SIGCSE 2001 Proceedings, pp 6-10.

• Event-driven Programming can be Simple Enough for CS 1
by Kim B. Bruce, Andrea Danyluk, and Thomas Murtagh.
ITiCSE 2001 Proceedings, pp. 1-4.

• Has Our Curriculum Become Math-Phobic? (an American Perspective)
by Kim B. Bruce, Charles Keleman, and Allen Tucker.
ITiCSE 2000 Proceedings, pp. 132-135

• Formal semantics and interpreters in a Principles of Programming Languages course
by Kim B. Bruce
Extended abstract. SIGCSE 99 pp. 331-335.

• Creating a new model curriculum: A rationale for Computing Curricula '91
by Kim B. Bruce.
Education and Computing, 7(1991), pp. 23-42.

• CS 137 course notes (Fall 1994), CS137.sit.hqx

Course notes and sample programs for Williams College CSCI 137, Programming paradigms and Data Structures. An unusual course whose content focusses on data structures, in which the intitial part of the course focusses on applications of data structures (using ML, a functional language), while the latter portion focusses on the implementation of the data structures using Object Pascal. This file, which is Stuffed and Binhexed, contains course lectures and sample programs. You will need a Mac to read it.

• Dataflow simulator, Dataflow.sit.hqx

A Macintosh application, written at Williams College, which simulates a dataflow computer. Includes documentation and sample programs.

• ## DETAILED ABSTRACTS OF PAPERS

1. Seeking Grace: A new object-oriented language for novices Andrew P. Black, Kim B. Bruce, Michael Homer, James Noble, Amy Ruskin, and Richard Yannow. Proceedings of SIGCSE Computer Science Education 2013. ACM, New York, NY, USA, 2013, pp. 129-134. pdf

Abstract We are designing a new object-oriented language, Grace, whose target audience is novices. Grace is intended to integrate proven new ideas in programming languages into a conceptually simple language that allows the instructor and students to focus on the essential complexities of program- ming, while supporting a variety of approaches to teaching.

2. Patterns as objects in grace. Michael Homer, James Noble, Kim B. Bruce, Andrew P. Black, and David J. Pearce. Proceedings of the 8th symposium on Dynamic languages (DLS '12). ACM, New York, NY, USA, 2012, pp. 17-28. pdf

Abstract 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). Grace is a new, dynamic, object-oriented language designed to support teaching: to this end, Grace needs to support both styles. We explain how this conflict can be resolved gracefully: by modelling patterns and cases as partial functions, reifying those functions as objects, and then building up com- plex patterns from simpler ones using pattern combinators. We describe the implementation of this design as an object-oriented framework, and a case study of its effectiveness.

3. Grace: the Absence of (Inessential) Difficulty. Andrew P. Black, Kim B. Bruce, Michael Homer, and James Noble Proceedings of the ACM international symposium on New ideas, new paradigms, and reflections on programming and software (Onward! '12). ACM, New York, NY, USA, 2012, pp. 85-98. pdf

Abstract We are engaged in the design of a small, simple program- ming language for teaching novices object-oriented programming. This turns out to be far from a small, simple task. We focus on three of the problems that we encountered, and how we believe we have solved them. The problems are (1) gracefully combining object initialization, inheritance, and immutable objects, (2) reconciling apparently irreconcilable views on type-checking, and (3) providing a family of languages, each suitable for students at different levels of mas- tery, while ensuring conceptual integrity of their designs. In each case our solutions are based on existing research; our contribution is, by design, consolidation rather than innovation.

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

5. On reacting to assertions and polar questions by Donka Farkas and Kim Bruce
Journal of Semantics. 27 (2010), pp. 81--118. Preprint available. Also pdf file of draft version.

Abstract The aim of this paper is to capture the similarities and differences between assertions and polar questions so as to be able to account for the systematic partial overlap that exists in reactions to these speech acts in English and beyond. We first discuss the discourse components we assume, and then define default assertions and default polar questions in a way that allows us to characterize two types of responses to these speech acts, confirming and reversing reactions. The common characteristics of assertions and polar questions are responsible for the fact that both allow these reactions; the differences between the two speech acts explain the different contextual effects confirming and reversing moves have depending on whether they react to an assertion or a polar question. We then examine the distribution of a set of 'polarity' particles in Romanian in terms of the notions defined in the rest of the paper, and end with a series of predictions concerning polarity particles across languages.

6. LOOJ: Weaving LOOM into Java by Kim B. Bruce and J. Nathan Foster
Extended abstract. Proceedings of ECOOP 2004. LNCS 3086, Springer-Verlag, pp. 390-414, 2004. pdf file.

Abstract LOOJ is an extension of Java obtained by adding bounded parametric polymorphism and new type expressions ThisClass and ThisType, which are similar to MyType in LOOM. Through examples we demonstrate the utility of this language even over very expressive extensions such as GJ. The LOOJ compiler generates standard JVML code and supports instanceof and casts for all types including type variables and the other new type expressions. The core of the LOOJ type system is sound, as demonstrated by a soundness proof for an extension of Featherweight GJ. This paper also highlights difficulties that arise from the use of both classes and interfaces as types in Java.

7. Some Challenging Typing Issues in Object-Oriented Languages, by Kim B. Bruce
Extended abstract. Electronic Notes in Theoretical Computer Science 82, no. 8 (2003). Last revised 6/2003. pdf file.

Abstract In this paper we discuss some of the remaining problems in the design of static type systems for object-oriented programming languages. We look at typing problems involved in writing a simple interpreter as a good example of a simple problem leading to difficult typing issues. The difficulties encountered seem to arise in situations where a programmer desires to simultaneously refine mutually interdependent classes and object types.

8. Semantics-Driven Language Design: Statically type-safe virtual types in object-oriented languages
by Kim B. Bruce and Joseph Vanderwaart
Proceedings of MFPS '99. Electronic Notes in Theoretical Computer Science, 82(8), 29 pages. Last revised 2/25/99.
dvi file, postscript

Abstract The virtual class construct was first introduced in the language Beta to provide added expressiveness when used with inheritance. Unfortunately, the virtual class construct in Beta is not statically type-safe. In this paper we show how a generalization of the semantics of object-oriented languages with a MyType construct leads to a variant of virtual classes which needs no run-time checks. This results in an object-oriented language in which both parametric types and virtual classes (or types) are well-integrated, and which is statically type-safe.

Keywords: Language design, semantics, virtual classes, parametric polymorphism, static type checking

9. Modules in LOOM: Classes are not enough
by Kim B. Bruce, Leaf Petersen, and Joseph Vanderwaart.
Extended abstract submitted to OOPSLA98. Last revised 4/13/98. dvi file, postscript

Abstract Pure object-oriented languages have tended to assume that classes can take the place of modules in programming in the large. We argue that modules are still needed in these languages and present the design of a module construct for our language LOOM which works well with the object-oriented paradigm. We discuss and illustrate the advantages of these modules over a class-only approach. In particular we illustrate the advantages of modules in supporting better control over information hiding, including the support of access like C++'s friends.

Keywords: Language design, modules.

10. A statically safe alternative to virtual types
by Kim B. Bruce, Martin Odersky, and Philip Wadler
ECOOP '98 Proceedings, LNCS 1445. pp 523-549. Last revised 4/1/98. dvi file, postscript

Abstract Parametric types and virtual types have recently been proposed as extensions to Java to support genericity. In this paper we investigate the strengths and weaknesses of each. We suggest a variant of virtual types which has similar expressiveness, but supports safe static type checking. This results in a language in which both parametric types and virtual types are well-integrated, and which is statically type-safe.

Keywords: Language design, virtual types, parametric polymorphism, static type checking

11. Increasing Java's expressiveness with ThisType and match-bounded polymorphism
by Kim B. Bruce
Draft. dvi file, postscript

Abstract This paper proposes some relatively minor additions to Java's syntax and semantics in order to increase the expressiveness of the language with little cost in semantic complexity. No changes are suggested that would invalidate or change the semantics of programs written in the current version of Java.

While the main point of the language extensions are to support parametric polymorphism, we also added features which provide better support for binary methods, a kind of method that is often difficult to support in a statically typed language. (See \cite{BinMeth} for an extensive discussion of the difficulties of statically type-checking binary methods.)

Briefly, the changes proposed are to add a ThisType' construct to represent the type of this'' (the name of the object executing a method), to provide a mechanism for the programmer to specify that a variable hold values of exactly the type given (and not a type that extends it), to reinterpret extends'' as matching'' rather than subtyping'', and to add a form of constrained polymorphism which depends on matching.

Category: Language design

12. Safe static type checking with systems of mutually recursive classes and inheritance
by Kim B. Bruce
Draft. dvi file, postscript

Abstract Virtual classes, which were first used in Beta \cite{VirtClass}, have recently been suggested by Thorup \cite{Thorup} as an extension to Java to support genericity. While virtual classes are a convenient mechanism to support simultaneous modification of mutually recursive classes, they rely on dynamic type checking for type safety. We suggest a variant which has similar expressiveness as virtual classes, but supports safe static type checking. To ease the comparison with earlier work we express our construct as an addition to Java, though similar constructs may be added to a variety of object-oriented languages. For example, this proposal can also be seen as a statically type-safe alternative to Eiffel's anchored types''.

Category: Language design

13. Comparing Object Encodings, by Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce.
Information and Computation 155(1999), pp 108-133 : comp.dvi, comp.ps, 23 pp.

ABSTRACT
Recent years have seen the development of several foundational models for statically typed object-oriented programming. But despite their intuitive similarity, differences in the technical machinery used to formulate the various proposals have made them difficult to compare.

Using the typed lambda-calculus \FOMEGASUB{} as a common basis, we now offer a detailed comparison of four models: (1) a recursive-record encoding similar to the ones used by Cardelli \cite{Cardelli88}, Reddy \cite{Reddy88->KaminReddy94,KaminReddy94}, Cook \cite{Cook89,CookCH90}, and others; (2) Hofmann, Pierce, and Turner's existential encoding \cite{PTSimple,HofmannPierce94}; (3) Bruce's model based on existential and recursive types \cite{Bruce92}; and (4) Abadi, Cardelli, and Viswanathan's type-theoretic encoding \cite{AbCardV} of a calculus of primitive objects.

Categories: Semantics, Foundations of object-oriented languages.

14. Subtyping is not a good Match'' for object-oriented languages, by Kim B. Bruce, Adrian Fiech, and Leaf Petersen.
Extended abstract appeared in ECOOP '97 Proceedings, LNCS 1241, Springer-Verlag, pp. 104-127: LOOM.dvi, LOOM.ps, 24 pp.

ABSTRACT
We present the design and rationale of a new statically-typed object-oriented language, LOOM. LOOM retains most of the features of the earlier language PolyTOIL. However the subtyping relation is dropped from LOOM in favor of the matching relation. Hash types'', which are defined in terms of matching, are introduced to provide some of the benefits of subtyping. These types can be used to provide support for heterogeneous data stuctures in LOOM. LOOM is considerably simpler than PolyTOIL, yet the language is just as expressive. The type system for the language is decidable and provably type safe. The addition of modules to the language provides better control over information hiding and allows the provision of access like that of C++'s friends.

Categories: Type systems and language design for object-oriented languages.

15. Typing in object-oriented languages: Achieving expressiveness and safety, by Kim B. Bruce.
Technical report: Static.dvi, Static.ps,33 pp, Lecture notes (postscript).

ABSTRACT
While simple static-typing disciplines exist for object-oriented languages like C++, Object Pascal, and Modula-3, they are often so restrictive that programmers are forced to by-pass the type system with type casts. Other languages allow more freedom, but require run-time checking to pick up the type errors that their more permissive systems missed.

This paper consists of a survey of problems (illustrated by a series of sample programs) with existing type systems, and suggests ways of improving the expressibility of these systems while retaining static type safety. In particular we will discuss the motivations behind introducing "MyType", "matching", and "bounded matching" into these type systems.

We also suggest a way of simplifying the resulting type system by replacing subtyping by a type system with a new type construct based on matching. Both systems provide support for binary methods, which are often difficult to support in statically-typed languages.

The intent is to avoid pages of type-checking rules and formal proofs, but instead explain why the problems are interesting via the series of sample programs. The technical details (including proofs of subject reduction and type safety) are available elsewhere.

Categories: Type systems for object-oriented languages.

16. PolyTOIL: A type-safe polymorphic object-oriented language
Kim B. Bruce, Angela Schuett, Robert van Gent, Adrian Fiech
ACM Transactions on Programming Languages and Systems (TOPLAS), 2003
ABSTRACT
In this paper we present the design of PolyTOIL, a provably type-safe polymorphic object-oriented programming language. PolyTOIL is designed to be significantly more expressive than statically-typed languages like C++. Innovative features include
17. A name for the (external) type of self, MyType, which provides extra flexibility in providing types for instance variables and methods, especially when used in conjunction with subclasses;
18. The ability to replace the types of methods by subtypes when redefining methods;
19. The separation of the definitions of type and subtype from implementation details. This allows:
• the definition of multiple classes generating objects of the same type,
• the definition of subclasses which do not generate subtypes.
20. The provision of bounded polymorphism based on matching'' which provides greater expressibility than bounded polymorphism based on subtypes.
21. Powerful modular type-checking rules for classes and subclasses that obviate the necessity of repeatedly type checking inherited methods.
22. A proof of the type safety of the language which is based on formal type-checking rules and an operational semantics.
23. The proof of type safety is obtained with the aid of a subject reduction theorem which ties together the type-checking rules with a (natural) operational semantics. The proof of subject reduction may be of independent interest in that it applies to an environment-based natural semantics for a polymorphic language.

Categories: Type systems, design and semantics of object-oriented languages.

24. On binary methods, by Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, The Hopkins Objects Group, Gary T. Leavens, and Benjamin Pierce.
Theory and Practice of Object Systems, 1(1995), pp. 221-242. binary.dvi , binary.ps

ABSTRACT
Giving types to binary methods causes significant problems for object-oriented language designers and programmers. This paper offers a comprehensive description of the problems arising from typing binary methods, and collects and contrasts diverse views and solutions. It summarizes the current debate on the problem of binary methods for a wide audience.

25. TOIL: A new Type-safe Object-oriented Imperative Language, by Kim B. Bruce and Robert van Gent,
Technical Report TOILwPf.dvi

ABSTRACT
In \cite{BrPOPL93}, the first author introduced the language TOOPLE, a statically-typed functional object-oriented programming language which has a number of desirable properties. In this and a series of other papers (\cite{Bruce92,BCDMMG,BrCrKan}), the denotational and natural semantics of TOOPLE have been presented and shown to be relatively consistent, subject-reduction and type-safety have been proven, and the type-checking problem has been shown to be decidable.

In this paper we introduce TOIL, a statically-typed object-oriented imperative language, which is based on the same semantic principles as TOOPLE and shares many of the same desirable properties. We include type-checking rules, an operational semantics, and prove a subject-reduction theorem for TOIL, showing that the operational semantics is type-safe.

This paper is an application of the theoretical work on the semantics of object-oriented programming languages done over the last decade to the design of real object-oriented programming languages.

26. A Paradigmatic Object-Oriented Programming Language: Design, Static Typing and Semantics, by Kim B. Bruce.
Journal of Functional Programming 4(1994), pp. 127-206: ObjDesign.dvi, ObjDesign.ps

ABSTRACT
In order 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 does not contain holes in the type system. A particular problem with statically type checking object-oriented languages is designing type-checking 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.

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 supported the language design by providing a means to prove that the type checking rules are sound, providing a guarantee 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 seems relatively straightforward.

27. Safe and decidable type checking in an object-oriented language, by Kim B. Bruce, Jon Crabtree, Allyn Dimock, Robert Muller, Thomas P. Murtagh, Robert van Gent.
OOPSLA '93 proceedings, pp. 29-46. OOPSLA.dvi

ABSTRACT
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_{\le}$. Unfortunately, it has recently been shown by Pierce (\cite{Pierce92}) that type checking $F_{\le}$ 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 \cite{Bruce92,BrPOPL93}, 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_{\le}$, 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 (which are in fact computable), and then using these two results to show that type checking is decidable. Interestingly, conditional statements introduce significant problems which necessitated the computation of generalized least upper bounds of types. The interaction of the least upper bounds with the implicit recursion in object and class definitions and the contravariant nature of function spaces makes the computation of appropriate least upper bounds more subtle than might be expected. Our algorithm fails to be polynomial in the size of the term because the size of the type of a term can be exponential in the size of the term. Nevertheless, it performs well in practice.

This paper concentrates on the language without instance variables, though the results can be extended to the full language, at the cost of some added complexity.

28. An operational semantics for TOOPLE: A statically-typed object-oriented programming language, by Kim B. Bruce, Jonathan Crabtree, and Gerald Kanapathy.
Proceedings of MFPS '93, LNCS 802, Springer-Verlag, 1994, pp. 603-626. TPLNatSem.dvi

ABSTRACT
In this paper we present an operational semantics for the language TOOPLE, a statically-typed, functional, object-oriented programming language which has a number of desirable properties. The operational semantics, given in the form of a natural semantics, is significantly simpler than the previous denotational semantics for the language. A subject reduction'' theorem for the natural semantics provides a proof that the language is type-safe. We also show that the natural semantics is consistent with the denotational semantics of the language.

29. Safe Type Checking in a Statically-Typed Object-Oriented Programming Language by Kim B. Bruce.
Proc ACM Symp. Principles of Programming Languages, 1993, pp. 285-298: TCPOPL.dvi

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

It has proved to be surprisingly difficult to design statically-typed object-oriented languages which are nearly as expressive as SmallTalk and yet have no holes in their typing systems. A particular problem with statically type checking object-oriented languages is determining whether a method provided in a superclass will continue to type check when inherited in a subclass. This problem is solved in our language by providing type checking rules which guarantee that a method which type checks as part of a class will type check correctly in all legal subclasses in which it is inherited. This feature enables library providers to provide only the interfaces of classes with executables and still allow users to safely create subclasses.

The design of TOOPL has been guided by an analysis of the semantics of the language, which is given in terms of a sufficiently rich model of the F-bounded second-order lambda calculus. This semantics supported the language design by provided a means of proving that the type-checking rules for the language are sound, ensuring that well-typed terms produce objects of the appropriate type. In particular, in a well-typed program it is impossible to send a message to an object which lacks a corresponding method.

30. PER models of subtyping, recursive types and higher-order polymorphism, by Kim B. Bruce and John Mitchell.
Proceedings of POPL '92, pp. 316-327: BrMitPOPL.dvi

ABSTRACT
We relate standard techniques for solving recursive domain equations to previous models with types interpreted as partial equivalence relations (per's) over a $D_\infty$ lambda model. This motivates a particular choice of type functions, which leads to an extension of such models to higher-order polymorphism. The resulting models provide natural interpretations for function spaces, records, recursively defined types, higher-order type functions, and bounded polymorphic types forall X <: Y. A where the bound may be of a higher kind. In particular, we may combine recursion and polymorphism in a way that allows the bound Y in forall X <: Y. A to be recursively defined. The model may also be used to interpret so-called F-bounded polymorphism. Together, these features allow us to represent several forms of type and type functions that seem to arise naturally in typed object-oriented programming.

31. The Equivalence of Two Semantic Definitions for Inheritance in Object-Oriented Languages, by Kim B. Bruce.
Proceedings of the MFPS '91 Conference, pp. 102-124: inherit.dvi

ABSTRACT
A simple language is presented which supports inheritance in object-oriented languages. Using this language, the definitions for the semantics of inheritance given in \cite{CookCH90} and \cite{MitchPOPL90} are compared and shown to be equivalent. The equivalence is shown by presenting and comparing two denotational semantics of the simple language which capture the essence of each of the earlier semantics.

32. Formal semantics and interpreters in a Principles of Programming Languages course
by Kim B. Bruce
Extended abstract. SIGCSE 99, pp 331-335. SIGCSEPL.ps.gz, SIGCSEPL.dvi.gz

ABSTRACT
It is unfortunate that in most computing curricula, the uses of theory and formalisms are limited to the algorithms and theory of computation courses. In fact, as indicated in the Logic in Computer Science'' panel BKLV98 in SIGCSE 97, logic and logic-related formalisms can play important parts of a wide variety of courses. In this paper we explain how logic-based ideas involving formal operational semantics and type-checking rules can play an important role in upper-level principles of programming languages courses.

33. Creating a new model curriculum: A rationale for Computing Curricula '91 , by Kim B. Bruce.
Education and Computing, 7(1991), pp. 23-42 IFIPCurric.ps.gz, IFIPCurric.dvi.gz

ABSTRACT
In 1988 the ACM and the IEEE Computer Society formed a Joint Curriculum Task Force to create a new model curriculum to replace Curriculum '88. Three years later the committee produced the report, titled Computing Curricula' 91. In this paper we discuss informally some of the considerations involved in creating the curriculum report, with the hopes that this will be helpful to anyone interested in implementing a curriculum in Computer Science based on the Task Force's report.

34. Has Our Curriculum Become Math-Phobic? (an American Perspective)
by Kim B. Bruce, Charles Keleman, and Allen Tucker.
ITICSE Proceedings, pp. 132-135 iticse.pdf.gz,

ABSTRACT
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.

35. A library to support a graphics based object-first approach to CS 1
by Kim B. Bruce, Andrea Danyluk, and Thomas Murtagh.
SIGCSE 2001 Proceedings, pp 6-10. SIGCSE2001Lib.dvi.gz, SIGCSE2001Lib.ps.gz, SIGCSE2001Lib.pdf,

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

36. Our Curriculum Has Become Math-Phobic!
by Kim B. Bruce, Charles Keleman, and Allen Tucker.
SIGCSE 2001 Proceedings, pp. 243-247. SIGCSE2001MathPhobic.dvi.gz, SIGCSE2001MathPhobic.ps.gz,

ABSTRACT
The paper \cite{Kelemen2000} 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.

37. Event-driven Programming can be Simple Enough for CS 1 by Kim B. Bruce, Andrea Danyluk, and Tom Murtagh.
ITiCSE 2001 proceedings, pp. 1-4.
eventsREZ.pdf

ABSTRACT
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.

38. Event-driven programming facilitates learning standard programming concepts by Kim B. Bruce, Andrea Danyluk, and Thomas Murtagh.
Proceedings of 2004 OOPSLA Educator's symposium, OOPSLA '04 companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications pp 96-100. Last revised 7/2004.
event2.pdf

ABSTRACT
We have designed a CS 1 course that integrates event-driven programming from the very start. In earlier papers we argued that event-driven programming is simple enough for CS 1 when introduced with the aid of a library that we have developed. In this paper we argue that early use of event-driven programming makes many of the standard topics of CS 1 much easier for students to learn by breaking them into smaller, more understandable concepts.

39. Controversy on How to Teach CS 1: A discussion on the SIGCSE-members mailing list
by Kim B. Bruce

ABSTRACT
A discussion took place on the SIGCSE mailing list in late March of 2004 that raised important issues on how to teach introductory courses using Java. This article attempts to summarize several of the important points raised during this discussion, among them whether or how objects should be taught early or late in a CS 1 course, or indeed whether object-oriented languages should be postponed until a second course.

40. Why Math?
by Kim B. Bruce, Scot Drysdale, Charles Kelemen, and Allen Tucker
CACM, September, 2003 pp. 41-44.
WhyMath.pdf
(C) ACM, 2003. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in CACM, Volume 46, Issue 9 (September 2003), pp. 40-44

ABSTRACT
The mathematical thinking, as well as the mathematics, in a computer science education prepares students for all stages of system development, from design to the correctness of the final implementation.

41. Why structural recursion should be taught before arrays in CS 1,
by Kim B. Bruce, Andrea Danyluk, and Thomas Murtagh.
Proceedings of the 2005 ACM Symposium on Computer Science Education, pp. 246-250, 2005.
p266-bruce.pdf

ABSTRACT
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.

42. A 2007 Model Curriculum for a Liberal Arts Degree in Computer Science,
by Liberal Arts Computer Science Consortium.
J. Educ. Resour. Comput. 7, 2 (Jun. 2007)
LACS_JERIC.pdf

(C) ACM, 2007. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in J. Educ. Resour. Comput. 7, 2 (Jun. 2007)

kim@cs.pomona.edu