Research Directed by Gary T. Leavens

This page summarizes the research directed by Gary T. Leavens at the University of Central Florida in the School of Electrical Engineering and Computer Science. (Research prior to July 2007 took place at Iowa State University, in the Department of Computer Science.) An up-to-date copy is available on the world wide web in the following URL.

  http://www.eecs.ucf.edu/~leavens/main.html

Also on-line is a a list of my students and former students with their research. You can also download a BibTeX file with entries for all my papers. See also the section below on how to get the papers mentioned.

You might also want to look in my home page, where there is:

• a general description of my research,
• a short list of representative publications, and
• a list of my other WWW pages.

Specification and Formal Methods

General

CS-TR-09-01 is a survey of behavioral interface specification languages.

Information hiding and visibility of specification constructs is the focus of TR06-28.

A roadmap for research related to verified software is found in TR06-21.

The ACL approach to preventing aliasing from repeated parameters is described in TR98-08a and the C/ACL compiler is described in TR01-11.

Ownership applied to specifications is the topic of several papers. TR02-02a (an expansion of TR01-03) describes an application of Peter Müller's dissertation work on modular specification of frame properties to JML. This is also the basis for the work on modular invariants.

Specification of superclasses to allow work on subclasses is the topic of TR #00-05 with Clyde Ruby; it describes a technique for reasoning about the correctness of subclasses.

The execution of specifications in the context of the language SPECS-C++ is the subject of TR #00-02, TR #97-12a, and TR #94-02b with Tim Wahls.

A translation of Z specifications into Larch is the subject of Hua Zhong's master's project.

Various specification enhancements found in Larch/C++ are described in TR #97-19.

Inheritance of specifications in an object-oriented context is discussed in a WIDL paper. This topic was further developed in an ICSE 1996 paper with Krishna Kishore Dhara (see below).

(See also the Larch FAQ and the work on JML.)

• C. A. R. Hoare, Jayadev Misra, Gary T. Leavens, and Natarajan Shankar. The Verified Software Initiative: A Manifesto. ACM Computing Surveys, 41(4):22:1-22:8, October 2009.
  http://dx.doi.org/10.1145/1592434.1592439
• Hridesh Rajan, Jia Tao, Steve Shaner, and Gary T. Leavens. Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services. In Giuseppe Castagna (ed.), Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, pages 333-347, March 2009. The original publication is available at springerlink.com from http://dx.doi.org/10.1007/978-3-642-00590-9_24.
  See also Department of Computer Science, Iowa State University, TR #08-07, July 2008. [TR abstract] [TR PDF]
• John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, and Matthew Parkinson. Behavioral Interface Specification Languages. School of EECS, University of Central Florida, CS-TR-09-01, March 2009. [abstract] [PDF]
• Gary T. Leavens and Peter Müller. Information Hiding and Visibility in Interface Specifications. Department of Computer Science, Iowa State University, TR #06-28, September 2006. [abstract] [PDF] [PostScript]
• Gary T. Leavens, Jean-Raymond Abrial, Don Batory, Michael Butler, Alessandro Coglio, Kathi Fisler, Eric Hehner, Cliff Jones, Dale Miller, Simon Peyton-Jones, Murali Sitaraman, Douglas R. Smith, and Aaron Stump. Roadmap for Enhanced Languages and Methods to Aid Verification. In Fifth International Conference on Generative Programming and Component Engineering (GPCE), pages 221-235, ACM, October 2006. http://doi.acm.org/10.1145/1173706.1173740
  Also Department of Computer Science, Iowa State University, TR #06-21, July 2006. [abstract] [PDF] [PostScript]
• Gary T. Leavens, K. Rustan M. Leino, and Peter Müller. Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing, 19(2):159--189, June 2007. The original publication is available at springerlink.com from http://dx.doi.org/10.1007/s00165-007-0026-7.
  Also Department of Computer Science, Iowa State University, TR #06-14a, May 2006, revised August 2006. [abstract] [Preprint PDF] [Preprint PS]
• Yoonsik Cheon, Yoshiki Hayashi, and Gary T. Leavens. A Thought on Specification Reflection. Department of Computer Science, Iowa State University, TR #03-16, December 2003. [abstract] [postscript] [PDF]
• Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular Invariants for Object Structures. ETH Zurich, Technical Report 424, October 2003. [abstract] [PDF]
• Gregory W. Kulczycki, Murali Sitaraman, William F. Ogden, and Gary T. Leavens. Reasoning about Procedure Calls with Repeated Arguments and the Reference-Value Distinction. Department of Computer Science, Iowa State University, TR #02-13a, December 2002, revised December 2003. [abstract] [postscript] [PDF]
• Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular Specification of Frame Properties in JML. Concurrency and Computation: Practice and Experience, 15(2):117-154, February, 2003.
  Also Department of Computer Science, Iowa State University, TR #02-02a, February 2002, revised October 2002. [abstract] [postscript] [PDF]
• Medhat G. Assaad and Gary T. Leavens. Alias-free parameters in C for Better Reasoning and Optimization. Department of Computer Science, Iowa State University, TR #01-11, November 2001. [abstract] [postscript] [PDF]
• Peter Müller, Arnd Poetzsch-Heffter, and Gary T. Leavens. Modular Specification of Frame Properties in JML. In the Formal Techniques for Java Programs 2001, workshop at ECOOP 2001.
  Also Department of Computer Science, Iowa State University, TR #01-03, April 2001. [abstract] [postscript] [PDF]
• Tim Wahls and Gary T. Leavens. Formal Semantics of an Algorithm for Translating Model-based Specifications to Concurrent Constraint Programs. Proceedings of the 16th ACM Symposium on Applied Computing, Las Vegas, Nevada USA, March 11-14, 2001, pp. 567-575.
• Clyde Ruby and Gary T. Leavens. Safely Creating Correct Subclasses without Seeing Superclass Code. In OOPSLA 2000 Conference Proceedings, pages 208-228. Volume 35, number 10 of ACM SIGPLAN Notices, October 2000.
  Also Department of Computer Science, Iowa State University, TR #00-05d, April 2000, revised April, June, July 2000. [abstract] [postscript] [PDF]
• Tim Wahls, Gary T. Leavens, and Albert L. Baker. Executing Formal Specifications with Concurrent Constraint Programming. Automated Software Engineering, 7(4):315-343, December, 2000.
  Also Department of Computer Science, Iowa State University, TR #97-12c, August 1997, revised June 1998, May, July 2000. [abstract] [postscript]
• Tim Wahls and Gary T. Leavens. Formal Semantics and Soundness of an Algorithm for Translating Model-based Specifications to Concurrent Constraint Programs. Department of Computer Science, Iowa State University, TR #00-02a, March 2000, revised August 2000. [abstract] [postscript]
• Gary T. Leavens and Olga Antropova. ACL -- Eliminating Parameter Aliasing with Dynamic Dispatch. Department of Computer Science, Iowa State University, TR #98-08a, July 1998, revised February 1999. [abstract] [postscript]
• Hua Zhong. LSL Traits for using Z with Larch. Department of Computer Science, Iowa State University, TR #97-22, December 1997. [abstract] [postscript]
• Gary T. Leavens and Albert L. Baker. Enhancing the Pre- and Postcondition Technique for More Expressive Specifications. In Jeannette M. Wing, James Woodcock, and Jim Davies (editors). FM'99 -- Formal Methods: World Congress on Formal Methods in Development of Computer Systems, Toulouse, France, September 1999, pages 1087-1106. Volume 1709 of Lecture Notes in Computer Science, Springer-Verlag, 1999. http://www.springerlink.com/content/74v251avr98krlmw
  Also: Department of Computer Science, Iowa State University, TR #97-19b, September 1997, revised February, June 1999.
• Gary T. Leavens and Clyde Ruby. Specification Facets for More Precise, Focused Documentation. In the Proceedings of the Eighth Annual Workshop on Software Reuse (WISR8), Columbus Ohio, March 1997.
  Also Department of Computer Science, Iowa State University, TR #97-04, January 1997. [abstract] [postscript]
• Gary T. Leavens and Jeannette M. Wing. Protective Interface Specifications. Formal Aspects of Computing, 10(1):59-75, January 1998. The original publication is available at springerlink.com from http://dx.doi.org/10.1007/PL00003926.
  An earlier version appears in Michel Bidoit and Max Dauchet (editors), TAPSOFT '97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, Lille, France, pages 520-534. Volume 1214 of Lecture Notes in Computer Science, Springer-Verlag, 1997.
• Tim Wahls, Albert L. Baker, and Gary T. Leavens. The Direct Execution of SPECS-C++: A Model-Based Specification Language for C++ Classes. Department of Computer Science, Iowa State University, TR #94-02b, February 1994, revised November 1994. [abstract] [postscript]
• Gary T. Leavens. Inheritance of Interface Specifications (Extended Abstract). In Proceedings of the Workshop on Interface Definition Languages, J. M. Wing, editor, pages 129-138. Volume 29, number 8, of ACM SIGPLAN Notices, August 1994. (Also Department of Computer Science, Iowa State University, TR #93-23, September 1993. [abstract] [postscript])
• Gary T. Leavens and Yoonsik Cheon. Overview and Specification of the Built-in Types in Little Smalltalk. Department of Computer Science, Iowa State University, TR #91-22a, October 1991, revised February 1994. [abstract] [postscript]
• Dennis de Champeaux, Pierre America, Derek Coleman, Roger Duke, Doug Lea, and Gary T. Leavens. Formal Techniques for OO Software Development. In OOPSLA '91 Proceedings, pages 166-170. Volume 26, number 11 of ACM SIGPLAN Notices, November 1991.

The JML Project

JML is a behavioral interface specification language tailored to the specification of Java modules. It combines the approaches of Eiffel and Larch, with some elements of the refinement calculus. Its home page is

  http://www.jmlspecs.org/

The Larch/C++ Project

Larch/C++ is a behavioral interface specification language tailored to the specification of C++ modules. Its home page is

  http://www.eecs.ucf.edu/~leavens/larchc++.html

You can get a beta-test release of Larch/C++ and papers on Larch/C++ by anonymous ftp from ftp.cs.iastate.edu in directory pub/larchc++.

Larch/Smalltalk

Larch/Smalltalk is a behavioral interface specification language tailored to the specification of Smalltalk modules. Its home page is

  http://www.eecs.ucf.edu/~leavens/larchSmalltalk.html

Yoonsik Cheon is the main designer of Larch/Smalltalk.

The current beta release of the Larch/Smalltalk system and some papers are available by anonymous ftp from ftp.cs.iastate.edu in directory pub/larchSmalltalk.

Larch/CORBA

The following paper gives the idea of designing Larch/CORBA, a behavioral interface specification language tailored to OMG's IDL.

• Gary T. Leavens and Yoonsik Cheon. Extending CORBA IDL to Specify Behavior with Larch. In OOPSLA '93 Workshop Proceedings: Specification of Behavioral Semantics in OO Information Modeling, pages 77-80. (Also Department of Computer Science, Iowa State University, TR #93-20, August 1993. [abstract] [text file])

More useful is the master's thesis of Gowri Sankar Sivaprasad, which gives a design of Larch/CORBA.

• Gowri Sankar Sivaprasad. Larch/CORBA: Specifying the Behavior of CORBA-IDL Interfaces. Department of Computer Science, Iowa State University, TR #95-27a, December 1995, revised December 1995. [abstract] [postscript]

Semantics

An introductory survey of class-based and algebraic models of objects that may be read as background to the rest of these is the following.

• Gary T. Leavens and Don Pigozzi. Class-Based and Algebraic Models of Objects. In Rance Cleaveland and Michael Mislove and Philip Mulry (eds.), US---Brazil Joint Workshops on the Formal Foundations of Software Systems, Electronic Notes in Theoretical Computer Science, vol. 14 [abstract]

Model Theory for ADTs

The following is recent work by Don Pigozzi, Krishna Kishore Dhara and myself on model theory of behavior for ADTs. It is used to study subtyping in TR96-15.

• Gary T. Leavens and Don Pigozzi. The Behavior-Realization Adjunction and Generalized Homomorphic Relations. Theoretical Computer Science, 177:183-216, 1997.
  A slightly extended version is Department of Computer Science, Iowa State University, TR #94-18b, September 1994, revised September 1994, July 1996. [abstract] [postscript]
• Gary T. Leavens and Krishna Kishore Dhara. Blended Algebraic and Denotational Semantics for ADT Languages with Mutable Objects. Department of Computer Science, Iowa State University, TR #93-21b, September 1993, revised March, September 1994. [abstract] [postscript]

Behavioral Subtyping

Types with Mutable Objects

An overview that ties together the ideas of supertype abstraction, behavioral subtyping, and specification inheritance is found in TR#06-20b with David Naumann, with a shorter and more mathematically refined version in TR#06-36. A presentation of these ideas in the context of JML is found in TR#06-22.

For historical perspective, see the survey of behavioral subtyping in the Foundations of Component-Based Systems book.

Work with Krishna Kishore Dhara on subtyping concerns types with mutable objects is listed in this subsection. The most recent work with Dhara is TR #01-02, which has a good explanation of the ideas. More detailed is his dissertation.

A shorter introduction to the idea of behavioral subtyping that may be more accessible is the ICSE 1996 paper (which appears with a correction as TR #95-20c). This paper describes the idea of specification inheritance and how it relates to behavioral subtyping. Its ideas were embodied in Larch/C++ and JML.

Also, note that TR #94-21b makes the following older TRs obsolete: TR #92-36 and TR #92-35. The work described in this part does not (yet) describe a specification language or a verification logic. Kishore's master's thesis can be had by requesting it by e-mail, but it is summarized in TR #92-36.

• Gary T. Leavens and David A. Naumann. Behavioral Subtyping is Equivalent to Modular Reasoning for Object-oriented Programs. Department of Computer Science, Iowa State University, TR #06-36, December 2006. [abstract] [PDF] [postscript]
• Gary T. Leavens. JML's Rich, Inherited Specifications for Behavioral Subtypes. In Zhiming Liu and He Jifeng (eds), Formal Methods and Software Engineering: 8th International Conference on Formal Engineering Methods (ICFEM), Macao, China, pages 2-34. Volume 4260 of Lecture Notes in Computer Science, Springer-Verlag, 2006.
  Also Department of Computer Science, Iowa State University, TR #06-22, August 2006. [abstract] [postscript] [PDF]
• Gary T. Leavens and David A. Naumann. Behavioral Subtyping, Specification Inheritance, and Modular Reasoning. Department of Computer Science, Iowa State University, TR #06-20b, July 2006, revised August, September 2006. [abstract] [postscript] [PDF]
• Krishna Kishore Dhara and Gary T. Leavens. Preventing Cross-Type Aliasing for More Practical Reasoning. Department of Computer Science, Iowa State University, TR #01-02a, March 2001, revised November 2001. [abstract] [postscript] [PDF]
• Gary T. Leavens and Krishna Kishore Dhara. Concepts of Behavioral Subtyping and a Sketch of Their Extension to Component-Based Systems. In Gary T. Leavens and Murali Sitaraman (eds.), Foundations of Component-Based Systems, chapter 6, pages 113-135. Cambridge University Press, New York, NY, 2000. [PDF], [postscript]
• Krishna Kishore Dhara. Behavioral Subtyping in Object-Oriented Languages. Department of Computer Science, Iowa State University, TR #97-09, May 1997. [abstract] [postscript] (117 pages).
• Krishna Kishore Dhara and Gary T. Leavens. Forcing Behavioral Subtyping Through Specification Inheritance. In Proceedings 18th International Conference on Software Engineering, Berlin, Germany, pages 258-267. IEEE, 1996.
  An extended and slightly revised version is Department of Computer Science, Iowa State University, TR #95-20c, August 1995, revised August and December 1995, March 1997. [abstract] [postscript]
• Krishna Kishore Dhara and Gary T. Leavens. Weak Behavioral Subtyping for Types with Mutable Objects. In S. Brookes, M. Main, A. Melton, and M. Mislove, editors, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference, Preliminary Proceedings, pages 269-290.
  The final version appears in S. Brookes, M. Main, A. Melton, and M. Mislove, editors, Mathematical Foundations of Programming Semantics, Eleventh Annual Conference. Volume 1 of Electronic Notes in Theoretical Computer Science, Elsevier, 1995.

Types with Immutable Objects

The IEEE Software and OOPSLA/ECOOP '90 papers are short summaries of this work. The MFPS paper with Don Pigozzi is also fairly short, and extends the results to higher types; it isolates the key mathematical idea. A development of this mathematical idea, which gives both a necessary and sufficient model-theoretic criterion for correct behavioral subtyping is found in TR96-15. The proof theory is studied in TR02-07.

• Gary T. Leavens and Don Pigozzi. Equational Reasoning with Subtypes. Department of Computer Science, Iowa State University, TR #02-07, July 2002. [abstract] [postscript] [PDF]
• Gary T. Leavens and Don Pigozzi. A Complete Algebraic Characterization of Behavioral Subtyping. Acta Informatica 36:617-663, 2000.
• Gary T. Leavens and William E. Weihl. Specification and Verification of Object-Oriented Programs Using Supertype Abstraction. Acta Informatica 32(8):705-778, November 1995. The original publication is available at springerlink.com from http://dx.doi.org/10.1007/BF01178658.
  
  A longer version of this paper is Gary T. Leavens and William E. Weihl. Subtyping, Modular Specification, and Modular Verification for Applicative Object-Oriented Programs. Department of Computer Science, Iowa State University, TR #92-28d, September 1992, revised September and October 1993, and January and September 1994. [abstract] [postscript]
• Gary T. Leavens and Don Pigozzi. Typed Homomorphic Relations Extended with Subtypes. In Stephen Brookes, editor, Mathematical Foundations of Programming Semantics '91, pages 144-167. Volume 598 of Lecture Notes in Computer Science. Springer-Verlag, 1992. [SpringerLink]
• Gary T. Leavens. Modular Specification and Verification of Object-Oriented Programs. IEEE Software, 8(4):72-80, July, 1991. http://doi.ieeecomputersociety.org/10.1109/52.300040
• Gary T. Leavens and William E. Weihl. Reasoning about Object-Oriented Programs that use Subtypes (extended abstract). In OOPSLA ECOOP '90 Proceedings, pages 212-223 (Volume 25, number 10 of ACM SIGPLAN Notices, October 1990). http://doi.acm.org/10.1145/97945.97970
• Gary T. Leavens. Modular Verification of Object-Oriented Programs with Subtypes. Department of Computer Science, Iowa State University, TR #90-09, July 1990. [abstract] [postscript]
• Gary T. Leavens, Verifying Object-Oriented Programs that use Subtypes. Massachusetts Institute of Technology, Laboratory for Computer Science, Technical Report TR-439, February 1989.

The last report mentioned above, MIT/LCS/TR-439, is my Ph.D. dissertation. To get it, check your library, or write to Publications, Laboratory for Computer Science, Massachusetts Institute of Technology, 545 Technology Sq., Cambridge, MA 02139. Their phone number is (617)253-5894. The cost was $16.00 US. But you probably don't need to do that, as the thesis was reworked in a different framework in ISU TR #90-09. The Acta Informatica paper is a summary of the thesis work; TR #92-28d contains that paper and additional omitted details.

Semantics of DFDs and their Execution

The first of the papers below, makes the second obsolete.

• Gary T. Leavens, Tim Wahls, and Albert L. Baker. Formal Semantics for Structured Analysis Style Data Flow Diagram Specification Languages. In ACM SAC'99 -- 1999 ACM Symposium on Applied Computing, San Antonio, February/March, 1999, pages 526--532.
• Gary T. Leavens, Tim Wahls, Albert L. Baker, and Kari Lyle. An Operational Semantics of Firing Rules for Structured Analysis Style Data Flow Diagrams. Department of Computer Science, Iowa State University, TR #93-28d, December 1993, revised December 1993, September 1994, June 1996, July 1996. [abstract] [postscript]
• Tim Wahls, Albert L. Baker, and Gary T. Leavens, An Executable Semantics for a Formalized Data Flow Diagram Specification Language. Department of Computer Science, Iowa State University, TR #93-27, November 1993. [abstract] [postscript]

Other Papers on Semantics

A summary of the talks given at the workshop Foundations of Object-Oriented Languages (Paris, July 1994) is available in the following.

• Giuseppe Castagna and Gary T. Leavens. Foundations of Object-Oriented Languages: 2nd Workshop report. Department of Computer Science, Iowa State University, TR #94-22, November 1994. [abstract] [postscript]

Programming Language Design

Aspect-Oriented Programming

See the page on More Modular Reasoning for Aspect-Oriented Programs for papers by Curtis Clifton, myself, and others related to aspect-oriented programming.

The MultiJava Project

MultiJava is an extension to Java that supports modular open classes and multiple dispatch. See the MultiJava publications page for other papers on MultiJava.

• Curtis Clifton, Todd Millstein, Gary T. Leavens, and Craig Chambers. MultiJava: Design Rationale, Compiler Implementation, and Applications. ACM TOPLAS, Volume 28, number 3 (May 2006), pages 517-575.
  Also Department of Computer Science, Iowa State University, TR #04-01b, January 2004, revised December 2004. [abstract] [PDF] [PostScript]
• Curtis Clifton, Gary T. Leavens, Craig Chambers, and Todd Millstein. MultiJava: Modular Open Classes and Symmetric Multiple Dispatch for Java. In OOPSLA 2000 Conference Proceedings, pages 130-145. Volume 35, number 10 of ACM SIGPLAN Notices, October 2000.
  Also Department of Computer Science, Iowa State University, TR #00-06a, April 2000, July 2000. [abstract] [postscript].

Papers on Type Systems

The two versions of ``A Type Notation for Scheme'' reflect an evolution of the type system, the report TR#05-18 is the latest of these.

• Gary T. Leavens, Curtis Clifton, and Brian Dorn. A Type Notation for Scheme. Department of Computer Science, Iowa State University, TR #05-18, August 2005. [abstract] [PDF] [postscript]
• Gary T. Leavens and Curtis Clifton. A Type Notation for Scheme. Department of Computer Science, Iowa State University, TR #05-03, February 2005. [abstract] [PDF] [postscript]
• Jianbing Chen. Dynamic Semantics and Type-checking of Tuple. Department of Computer Science, Iowa State University, TR #98-10, December 1998. [abstract] [postscript].
• Gary T. Leavens and Todd D. Millstein. Multiple Dispatch as Dispatch on Tuples. In OOPSLA '98 Proceedings, pages 374-387 (Volume 33, number 10 of ACM SIGPLAN Notices October 1998). http://doi.acm.org/10.1145/286936.286977
  Also Department of Computer Science, Iowa State University, TR #98-03b, April 1998, Revised May 1998, July 1998. [abstract] [postscript].
• Craig Chambers and Gary T. Leavens. BeCecil, A Core Object-Oriented Language with Block Structure and Multimethods: Semantics and Typing. Presented at the The Fourth International Workshop on Foundations of Object-Oriented Languages FOOL 4, Paris, France.
  An extended and slightly revised version is Department of Computer Science, Iowa State University, TR #96-17a, December 1996, revised April 1997. [abstract] [postscript (101 pages)]. The main body and just the appendix sections are also available.
• Steven Jenkins and Gary T. Leavens. Polymorphic Type-Checking in Scheme. Computer Languages, 22(4): 215-223, 1996.
  Also Department of Computer Science, Iowa State University, TR95-21a, August 1995, revised May 1996. [abstract] [postscript]
• Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, The Hopkins Objects Group, Gary T. Leavens, and Benjamin Pierce. On Binary Methods. Theory and Practice of Object Systems 1(3):221-242, 1995.
  Also Department of Computer Science, Iowa State University, TR95-08a, May 1995, revised December 1995. [abstract] [postscript]
• Craig Chambers and Gary T. Leavens. Towards Safe Modular Extensible Objects. Department of Computer Science, Iowa State University, TR #94-17a, August 1994. [abstract] [postscript]
• Craig Chambers and Gary T. Leavens. Typechecking and Modules for Multimethods. ACM Transactions on Programming Languages and Systems, 17(6):805-843, November 1995. http://doi.acm.org/10.1145/218570.218571
  The longer version (with an appendix of formal proofs) is Department of Computer Science, Iowa State University, TR #95-19, August 1995. [abstract] [postscript]
• Craig Chambers and Gary T. Leavens. Typechecking and Modules for Multi-Methods. In OOPSLA '94 Conference Proceedings, pages 1-15. Volume 29, number 10 of ACM SIGPLAN Notices, October 1994. http://doi.acm.org/10.1145/191080.191083
  A longer version (with formal proofs) is Department of Computer Science, Iowa State University, TR #94-03a, March 1994, revised August 1994. [abstract] [postscript]

Other Papers on Programming Language Design

• Gary T. Leavens. Introduction to the Literature on Semantics. Department of Computer Science, Iowa State University, TR #94-15, August 1994. [abstract] [postscript] [PDF]
• Gary T. Leavens. Introduction to the Literature On Programming Language Design. Department of Computer Science, Iowa State University, TR #93-01b, January 1993, revised January 1994 and February 1996. [abstract] [postscript]
• Gary T. Leavens, Introduction to the Literature on Object-Oriented Design, Programming, and Languages. OOPS Messenger, 2(4):40-53, October 1991.
• Barbara Liskov, Mark Day, Maurice Herlihy, Paul Johnson, Gary T. Leavens (editor), Robert Scheifler, and William Weihl. Argus Reference Manual. Massachusetts Institute of Technology, Laboratory for Computer Science, Technical Report TR-400, October 1987. [postscipt]

Other Papers

Teaching Computer Science

• Gary T. Leavens. Use Concurrent Programming Models to Motivate Teaching of Programming Languages. In Programming Languages Curriculum Workshop 2008, pages 93-98. Volume 43, number 11 of ACM SIGPLAN Notices, Nov. 2008.
  http://doi.acm.org/10.1145/1480828.1480849
  Also School of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-08-04a, April 2008, revised May 2008. [abstract] [Preprint PDF]
• Gary T. Leavens. Following the Grammar. School of Electrical Engineering and Computer Science, University of Central Florida, CS-TR-07-10c, September 2007, revised October, November 2007, October 2009. [abstract] [PDF] [postscript]
• Gary T. Leavens. Following the Grammar. Department of Computer Science, Iowa State University, TR #05-02a, February 2005, revised January 2006. [abstract] [PDF] [postscript]
• Gary T. Leavens, Albert L. Baker, Vasant Honavar, Steven M. LaValle, Gurpur Prabhu. Programming is Writing: Why Student Programs must be Carefully Evaluated. Mathematics and Computer Education, 32(3):284-295, Fall 1998.
• Gary T. Leavens. A Physical Example for Teaching Curried Functions. Mathematics and Computer Education, 30(1):51-60, Winter 1996.
• Gary T. Leavens. Aiding Self-motivation with Readings in Introductory Computing. Mathematics and Computer Education, 29(2):124-133, 1995.
• Albert L. Baker, David Fernandez-Baca, and Gary T. Leavens. Course Specifications for New Introductory Courses: Computer Science 227X and 228X. Department of Computer Science, Iowa State University, TR #92-09, April 1992. [abstract] [postscript]

The 3x+1 Problem

• Gary T. Leavens and Mike Vermeulen, 3x+1 Search Programs. Computers and Mathematics with Applications, 24(11):79-99, December 1992.
• Gary T. Leavens. A Distributed Search Program for the 3x+1 problem. Department of Computer Science, Iowa State University, TR #89-22, November 1989. [abstract] [postscript]

Miscellaneous

• Kristina P. Boysen and Gary T. Leavens. Automatically generating consistent graphical user interfaces using a parser generator. Department of Computer Science, Iowa State University, TR #04-07a, August 2004, revised November 2005. [abstract] [PDF]
• Gary T. Leavens. Fields in Physics are like Curried Functions, or Physics for Functional Programmers. Department of Computer Science, Iowa State University, TR #94-06b, April 1994, revised May 1994. [abstract] [postscript]

How to get Papers Mentioned

Although it might violate the copyright laws, if you don't have a published paper in your library, you can probably get some version of it as an Iowa State University (ISU) Computer Science TR. (This is not to encourage you to violate the copyright law, however.) All ISU Com S TRs, including many old versions, should be available by the following means.

Through the web

You can get TRs from the department's archives server via the URL: http://archives.cs.iastate.edu/.

Electronic mail

Send a message with body

   send TR catalog

to almanac@cs.iastate.edu to see the catalog and instructions.

Anonymous ftp.

Use ftp to connect to ftp.cs.iastate.edu, login as user anonymous, with your e-mail address as the password. The TRs are in the directory pub/techreports with subdirectory TR90-09 holding TR 90-09, etc. (Omit any letter code. For example, TR93-18a is in directory TR93-18.)

Contact Information

Gary T. Leavens
University of Central Florida
School of Electrical Engineering and Computer Science, Building 116
4000 Central Florida Blvd.,
Orlando, Florida 32816-2362 USA

e-mail: leavens@eecs.ucf.edu
Phone: +1-407-823-4758 / fax: +1-407-823-5419

Last update $Date: 2009/10/21 14:42:55 $