Publications of Stephen J. Garland

2013

Stephen J. Garland, Robert N. Block, and George C. Conant, Multiple Synchronized Views for Creating, Analyzing, Editing, and Using Mathematical Formulas, United States Patent No. 8,510,650, August 13, 2013. [PDF]

2011

Nancy A. Lynch, Stephen J. Garland, Dilsun Kaynar, Laurent Michel, and Alex Shvartsman, The Tempo Language User Guide and Reference Manual, MIT Computer Science and Artificial Intelligence Laboratory, Cambridge, Massachusetts, October 2011. [PDF]

2005

Stephen J. Garland, Dilsun Kaynar, Nancy A. Lynch, Joshua A. Tauber, and Mandana Vaziri, TIOA Tutorial, MIT Computer Science and Artificial Intelligence Laboratory, Cambridge, Massachusetts, May 2005. [PDF]

Dilsun Kaynar, Nancy Lynch, Sayan Mitra, and Stephen Garland, The TIOA Language, MIT Computer Science and Artificial Intelligence Laboratory, Cambridge, Massachusetts, May 2005. [PDF]

2004

MIT Computer Science and Artificial Intelligence Laboratory, MIT Project Oxygen: Pervasive Human-Centered Computing, 2000–2004. Editor. [Website]

Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kirli, and Nancy Lynch, "Using simulated execution in verifying distributed algorithms," Software Tools for Technology Transfer 6:1, Lenore D. Zuck, Paul C. Attie, Agostino Cortesi, and Supratik Mukhopadhyay (editors), pages 67–76. Springer-Verlag, July 2004. [Abstract, PDF]

Joshua Tauber and Stephen J. Garland, Definition and expansion of composite automata in IOA, Technical Report MIT-CSAIL-TR-2004-048, MIT Computer Science and Artificial Intelligence Laboratory, Cambridge, Massachusetts, July 2004. [Abstract, PDF]

2003

Stephen J. Garland, Nancy A. Lynch, Joshua A. Tauber, and Mandana Vaziri, IOA User Guide and Reference Manual, MIT Computer Science and Artificial Intelligence Laboratory, Cambridge, Massachusetts, August 14, 2003. [PDF]

Toh Ne Win, Michael D. Ernst, Stephen J. Garland, Dilsun Kirli, and Nancy Lynch, "Using simulated execution in verifying distributed algorithms," VMCAI, pages 283–297, New York, January 9–11, 2003.

2002

Stephen J. Garland, "Designing reliable distributed systems," Byte, pages 41–48, Spring 2002. [PDF]

Andrej Bogdanov, Stephen J. Garland, and Nancy A. Lynch, "Mechanical translation of I/O automata specifications into first-order logic," Formal Techniques for Networked and Distributed Systems — FORTE 2002, Doron A. Peled and Moshe Y. Vardi (editors), Lecture Notes in Computer Science 2529, pages 364–368, Houston, TX, November 11-14, 2002. IFIP WG 6.1, Springer-Verlag. [PDF]

Toh Ne Win, Michael D. Ernst, and Stephen J. Garland, "Connecting specifications, executions, and proofs: Reducing human interaction in theorem proving," MIT Laboratory for Computer Science (unpublished), October 2002. [PDF]

Dilsun Kirli Kaynar, Anna Chefter, Laura Dean, Stephen J. Garland, Nancy A. Lynch, Toh Ne Win, and Antonio Ramirez-Robredo, "Simulating nondeterministic systems at multiple levels of abstraction," CONCUR 2002 Tools Day, Brno, Czech Republic, August 4, 2002. [PDF]

Dilsun Kirli Kaynar, Anna Chefter, Laura Dean, Stephen J. Garland, Nancy A. Lynch, Toh Ne Win, and Antonio Ramirez-Robredo, The IOA Simulator, Technical Report MIT-LCS-TR-843, MIT Laboratory for Computer Science, Cambridge, Massachusetts, July 2002. [PDF]

2001

Stephen J. Garland and Nancy A. Lynch, Model-Based Software Design and Validation, United States Patent No. 6,289,502, September 11, 2001. [PDF]

2000

Stephen J. Garland and Nancy A. Lynch, "Using I/O automata for developing distributed systems," Foundations of Component-Based Systems, Gary T. Leavens and Murali Sitaraman (editors), pages 285–312, Cambridge University Press, 2000. [Abstract, PDF]

1999

Erik L. Nygren, Stephen J. Garland, and M. Frans Kaashoek, "PAN: A high-performance active network node supporting multiple mobile code systems," OpenArch '99, New York, 1999. IEEE Communications Society.

1998

Stephen J. Garland and Nancy A. Lynch, The IOA Language and Toolset: Support for Designing, Analyzing, and Building Distributed Systems, Technical Report MIT-LCS-TR-762, MIT Laboratory for Computer Science, Cambridge, Massachusetts, August 1998. [Abstract, PDF]

Li-Wei Lehman, Stephen J. Garland, and David L. Tennenhouse, "Active reliable multicast," Infocom '98, San Francisco, April 1998. IEEE Communications Society. [Abstract, PDF]

1997

Stephen J. Garland, Nancy A. Lynch, and Mandana Vaziri, IOA: A Formal Language for Input/Output Automata, MIT Laboratory for Computer Science, 1997.  Superseded by MIT-LCS-TR-762, 1998.

1996

Tsvetomir P. Petrov, Anya Pogosyants, Stephen J. Garland, Victor Luchangco, and Nancy A. Lynch, "Computer-assisted verification of an algorithm for concurrent timestamps," Formal Description Techniques IX: Theory, Application, and Tools (FORTE/PSTV), Reinhard Gotzhein and Jan Bredereke (editors), pages 29–44, Kaiserslautern, Germany, October 8–11, 1996. Chapman & Hall. [Abstract, PDF]

Stephen J. Garland and Deepak Kapur, "A practical ordering for AC rewrite systems," MIT Laboratory for Computer Science (unpublished), 1996. [Abstract, PDF]

1995

Stephen J. Garland and John V. Guttag, "Systematic Program Development," Laboratory for Computer Science Progress Report, July 1994 – June 1995, Vol. 32, pages 227–233. Massachusetts Institute of Technology, 1995.

1994

Stephen J. Garland and John V. Guttag, "Systematic Program Development," Laboratory for Computer Science Progress Report, July 1993 – June 1994, Vol. 31. Massachusetts Institute of Technology, 1994.

Victor Luchangco, Ekrem Söylemez, Stephen Garland, and Nancy Lynch, "Verifying timing properties of concurrent algorithms," FORTE '94: Seventh International Conference on Formal Description Techniques, pages 259–273, Berne, Switzerland, October 4–7, 1994. Chapman & Hall. [Abstract, PDF]

1993

Stephen J. Garland and John V. Guttag, "Systematic Program Development," Laboratory for Computer Science Progress Report, July 1992 – June 1993, Vol. 30. Massachusetts Institute of Technology, 1993.

Stephen J. Garland, John V. Guttag, and James J. Horning, "An overview of Larch," Functional Programming, Concurrency, Simulation, and Automated Reasoning, Peter F. Lauer (editor), Lecture Notes in Computer Science 693, pages 329–348. Springer-Verlag, 1993. [Abstract, PDF]

John V. Guttag and James J. Horning, editors, Larch: Languages and Tools for Formal Specification, Texts and Monographs in Computer Science. Springer-Verlag, 1993. With Stephen J. Garland, Kevin D. Jones, Andrés Modet, and Jeannette M. Wing. [PDF]

James B. Saxe, Stephen J. Garland, John V. Guttag, and James J. Horning, "Using transformations and verification in circuit design," Formal Methods in System Design 3:3 (December 1993), pages 181–209. [Abstract, PDF]

Jørgen F. Søgaard-Anderson, Stephen J. Garland, John V. Guttag, Nancy A. Lynch, and Anya Pogosyants, "Computed-assisted simulation proofs," Fifth Conference on Computer-Aided Verification (CAV '03), Costas Courcoubetis (editor), Lecture Notes in Computer Science 697, pages 305–319, Elounda, Greece, June 1993. Springer-Verlag. [Abstract, PDF]

1992

Stephen J. Garland and John V. Guttag, "Systematic Program Development," Laboratory for Computer Science Progress Report, July 1991 – June 1992, Vol. 29. Massachusetts Institute of Technology, 1992.

James B. Saxe, Stephen J. Garland, John V. Guttag, and James J. Horning, "Using transformations and verification in circuit design," Designing Correct Circuits, IFIP Transactions A-5, Lyngby, Denmark, January 6–8, 1992. North-Holland. Also published as Digital Equipment Corporation Systems Research Center Report 78, 1991.

Jørgen Staunstrup, Stephen J. Garland, and John V. Guttag, "Mechanized verification of circuit descriptions using the Larch Prover," Theorem Provers in Circuit Design, Victoria Stavridou, Thomas F. Melham, and Raymond T. Boute (editors), IFIP Transactions A-10, pages 277–299, Nijmegen, The Netherlands, June 22–24, 1992. North-Holland. [Abstract, PDF]

Katherine A. Yelick and Stephen J. Garland, "A parallel completion procedure for term rewriting systems," Eleventh International Conference on Automated Deduction, Lecture Notes in Computer Science, pages 109–123, Sarasota Springs, NY, June 1992. Springer-Verlag. [Abstract, PDF]

1991

Stephen J. Garland and John V. Guttag, A Guide to LP: the Larch Prover, MIT Laboratory for Computer Science, December 1991. Also published as Digital Equipment Corporation Systems Research Center Report 82, 1991. [Abstract]

Stephen J. Garland and John V. Guttag, "Systematic Program Development," Laboratory for Computer Science Progress Report, July 1990 – June 1991, Vol. 28, pages 179–186. Massachusetts Institute of Technology, 1991.

1990

Stephen J. Garland and John V. Guttag, "Using LP to debug specifications," Programming Concepts and Methods, Sea of Galilee, Israel, April 2–5, 1990. IFIP WG 2.2/2.3, North-Holland.

Stephen J. Garland and John V. Guttag, "Systematic Program Development," Laboratory for Computer Science Progress Report, July 1989 – June 1990, Vol. 27, pages 143–156. Massachusetts Institute of Technology, 1990.

Stephen J. Garland, John V. Guttag, and James J. Horning, "Debugging Larch Shared Language specifications," IEEE Transactions on Software Engineering 16:9, pages 1044–1057, September 1990. Also published as Digital Equipment Corporation Systems Research Center Report 60, 1990.

1989

Stephen J. Garland and John V. Guttag, "An overview of LP, the Larch Prover," Third International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 355, pages 137–151, Chapel Hill, NC, April 1989. Springer-Verlag.

Stephen J. Garland and John V. Guttag. "Systematic Program Development," Laboratory for Computer Science Progress Report, July 1988 – June 1989, Vol. 26, pages 143–154. Massachusetts Institute of Technology, 1989. [PDF]

Jørgen Staunstrup, Stephen J. Garland, and John V. Guttag, "Localized verification of circuit descriptions," Automatic Verification Methods for Finite State Systems, Lecture Notes in Computer Science 407, pages 349–364, Grenoble, France, June 1989. Springer-Verlag. [PDF]

1988

Stephen J. Garland, "Advanced Placement Computer Science," MIT Laboratory for Computer Science (unpublished), 1988.

Stephen J. Garland and John V. Guttag, "Inductive methods for reasoning about abstract data types," Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 219–228, San Diego, CA, January 1988. [Abstract, PDF]

Stephen J. Garland and John V. Guttag, "LP: The Larch Prover," Ninth International Conference on Automated Deduction, Lecture Notes in Computer Science 310, pages 748–749, Argonne, Illinois, May 1988. Springer-Verlag.

Stephen J. Garland and John V. Guttag, "Systematic Program Development," Laboratory for Computer Science Progress Report, July 1987 – June 1988, Vol. 25. Massachusetts Institute of Technology, 1988.

Stephen J. Garland, John V. Guttag, and Jørgen Staunstrup, "Verification of VLSI circuits using LP," The Fusion of Hardware Design and Verification, pages 329–345, Glasgow, Scotland, July 4–6, 1988. IFIP WG 10.2, North Holland. [Abstract, PDF]

1987

Stephen J. Garland and John V. Guttag, "Semantic analysis of formal specifications," MIT Laboratory for Computer Science (unpublished), 1987.

Stephen J. Garland and John V. Guttag, "Systematic Program Development," Laboratory for Computer Science Progress Report, July 1986 – June 1987, Vol. 24, pages 167–179. Massachusetts Institute of Technology, 1987.

Stephen J. Garland and John V. Guttag, "Why induct inductionlessly when you could induct inductively," MIT Laboratory for Computer Science (unpublished), 1987.

1986

Stephen J. Garland, Introduction to Computer Science with Applications in Pascal, Addison-Wesley, Reading, MA, 1986.

Stephen J. Garland, Instructor's Guide to Accompany Introduction to Computer Science with Applications in Pascal, Addison-Wesley, Reading, MA, 1986. [PDF]

Stephen J. Garland and John V. Guttag, "Systematic Program Development," Laboratory for Computer Science Progress Report, July 1985 – June 1986, Vol. 23, pages 183–195. Massachusetts Institute of Technology, 1986.

1984

Stephen J. Garland, "Advanced Placement Computer Science," Computers in Mathematics Education, Viggo P. Hansen and Marilyn J. Zweng (editors), pages 194–201. Yearbook of the National Council of Teachers of Mathematics, 1984. [PDF]

Stephen J. Garland, "Languages for first courses in computer science: Basic," Abacus 1:4, pages 39–49, Summer 1984.

Stephen J. Garland, "Languages for first courses in computer science: Rebuttals," Abacus 2:1, pages 46–47, Fall 1984.

1983

The College Board, Teacher's Guide for Advanced Placement Courses in Computer Science, The College Board, 1983. 121 pages. Major contributor.

Stephen J. Garland, "The role of language in teaching programming," Proceedings of NECC/5, National Educational Computing Conference, June 6-8, 1983, Baltimore, Maryland, page 1. [Abstract]

Stephen J. Garland and Donald L. Kreider, "Problems of implementing a new mathematics curriculum," The Future of College Mathematics: Proceedings of a Conference-Workshop on the First Two Years of College Mathematics, Anthony Ralston and Gail S. Young (editors), pages 209–221, Springer-Verlag, 1983.

1982

Stephen J. Garland, editor, Advanced Placement Course Description: Computer Science, The College Board, 1982.

Stephen J. Garland, Introduction to Computing and Basic Programming, Program in Computer and Information Science, Dartmouth College, 1982.

1981

Committee on the Undergraduate Program in Mathematics, Recommendations for a General Mathematical Sciences Program, Mathematical Association of America, 1981. Member, Computer Science Subpanel.

1980

Gordon M. Bull and Stephen J. Garland, A Specification for Dartmouth BASIC, Version 7. Technical Report TM112, Kiewit Computation Center, Dartmouth College, Hanover, NH, 1980.

Stephen J. Garland, editor, Draft Proposed American National Standard for Basic, ANSI/X3J2, 1980. Documents 1979/08, 1979/51, 1980/50, 1980/64.

Stephen J. Garland, Donald L. Kreider, and Robert W. Ritchie, Recursive Functions and Effective Computability, Department of Mathematics, Dartmouth College, 1980.

1979

Stephen J. Garland, Mathematical Logic, Department of Mathematics, Dartmouth College, 1979, 229 pages.

Stephen J. Garland and A. Kent Morton, "A new master's degree program at Dartmouth College," ACM SIGCSE Bulletin 11:4, pages 25–26, December 1979. [PDF]

1978

William Y. Arms and Stephen J. Garland, A Preview of Basic 7, Technical Report SP047, Kiewit Computation Center, Dartmouth College, Hanover, NH, 1978.

Stephen J. Garland, editor, American National Standard for Minimal Basic, ANSI X3.60–1978, American National Standards Institute, 1978. Also available as Standard ECMA-55, Minimal Basic, European Computer Manufacturers Association, January 1978. [PDF]

Stephen J. Garland, "Why and how should colleges teach computing," Proceedings of the Conference on Prospects in Mathematics Education in the 1980's (PRIME-80), pages 64–68. Mathematical Association of America, 1978.

1976

Dorothy E. Denning, Peter J. Denning, Stephen J. Garland, Michael A. Harrison, and Walter L. Ruzzo, Proving protection systems safe, Technical Report CSD TR 709, Purdue University, November 1976.

Stephen J. Garland, Structured Programming, Graphics, and BASIC, Technical Report SP028, Kiewit Computation Center, Dartmouth College, Hanover, NH, 1976.

Stephen J. Garland and Christine Thompson, DTSS RUNOFF*** Reference Manual, Technical Report TM005, Kiewit Computation Center, Dartmouth College, Hanover, NH, 1976.

1975

Stephen J. Garland, editor, Calculus and Computing, American Mathematical Society, Mathematical Association of America, 1975.

Stephen J. Garland, "Where, when, and why should computers be used in education?," Man and Computer, pages 97–103. North-Holland, 1975.

Stephen J. Garland, Review of "Indescribability and the continuum" by Kenneth Kunen, The Journal of Symbolic Logic 40:4, page 632, December 1975. [PDF]

1974

Stephen J. Garland, "Second-order cardinal characterizability," Axiomatic Set Theory, Proceedings of Symposia in Pure Mathematics, Vol. XII, part 2, pages 127–146. American Mathematical Society, 1974. [PDF]

Stephen J. Garland, Review of "On limits of sequences of hyperarithmetical functionals and predicates" by Hisao Tanaka and "A note on the effective descriptive set theory" by Tosiyuki Tugué, Hisao Tanaka. The Journal of Symbolic Logic 39:2, pages 344–345, June 1974. [PDF]

Stephen J. Garland and Arthur W. Luehrmann, "Graphics in the BASIC language," Computer Graphics (quarterly report of SIGGRAPH-ACM) 8:3, pages 1–8, 1974.

1973

Gordon M. Bull, William Freeman, and Stephen J. Garland, Specification for Standard BASIC, National Computing Centre, Manchester, England, 1973.

Stephen J. Garland, Dartmouth BASIC: A specification, Technical Report TM028, Kiewit Computation Center, Dartmouth College, Hanover, NH, 1973.

Stephen J. Garland and David C. Luckham, "Program schemes, recursion schemes, and formal languages," Journal of Computer and System Sciences 7, pages 119–160, 1973.

1972

Committee on the Undergraduate Program in Mathematics, Recommendations on Undergraduate Mathematics Courses Involving Computing, A Report of the Panel on the Impact of Computing on Mathematics Courses, Mathematical Association of America, 1972. Panel Member.

Stephen J. Garland, "Generalized interpolation theorems," The Journal of Symbolic Logic 37, pages 343–351, 1972. [PDF]

Stephen J. Garland and David C. Luckham, "On the equivalence of schemes," Fourth Annual ACM Symposium on the Theory of Computing, pages 65–72, 1972.

Stephen J. Garland and David C. Luckham, "Translating recursion schemes into program schemes," ACM Conference on Proving Assertions about Programs, pages 83–96, 1972.

1971

Stephen J. Garland, Review of "On the uniformization principle" by Yoshindo Suzuki, The Journal of Symbolic Logic 36:4, page 687, December 1971. [PDF]

Stephen J. Garland, Review of "A complete classification of the Δ1/2-functions" by Yoshindo Suzuki, The Journal of Symbolic Logic 36:4, page 688, December 1971. [PDF]

1970

Stephen J. Garland, Specifications for Executive Commands, Technical Report TM059, Kiewit Computation Center, Dartmouth College, Hanover, NH, 1970.

1969

Stephen J. Garland, Background User's Manual, Technical Report TM008, Kiewit Computation Center, Dartmouth College, Hanover, NH, 1969.

Stephen J. Garland, Review of "Inductively defined sets of natural numbers" by C. Spector. The Journal of Symbolic Logic 34:2, pages 295–296, June 1969. [PDF]

Stephen J. Garland and John S. McGeachie, Multiple terminal programming, Technical Report TM009, Kiewit Computation Center, Dartmouth College, Hanover, NH, 1969.

1967

Stephen J. Garland, Second-Order Cardinal Characterizability, PhD Thesis, University of California at Berkeley, 1967. [Abstract]

1964

Stephen J. Garland, Anthony W. Knapp, and Thomas E. Kurtz, Algol for the LGP-30, Computation Center, Dartmouth College, 1962-63.
[
Abstract, PDF for ALGOL for the LGP-30, A Comparison (1962), PDF for Procedure Manual for ALGOL-30 (CCM-5, 1962), PDF for A Manual for SCALP, a Self Contained Algol Processor for the LGP-30 (1962), PDF for SCALP Block Diagrams (CCM-8A, 1963), PDF for SCALP Coding Sheets (CCM-8B, 1963), PDF for A Manual for SCALP, being a Self Contained Algol Processor for the General Precision LGP-30 (CCM-7A, 1964), PDF for the Royal McBee LGP-30 Operations Manual (1959)]

Julia Robinson, Mathematical logic, Lecture Notes for Mathematics 225 by Stephen J. Garland, Department of Mathematics, University of California at Berkeley, 1963-1964, 209 pages. [Abstract, PDF]

1963

Stephen J. Garland, Arithmetic functions on the constructively accessible ordinal numbers, Bachelor's Thesis, Department of Mathematics, Dartmouth College, 1963.

Peter Robinson, Robin Robinson, and Stephen J. Garland, "Preparation of beta diagrams in structural geology by a digital computer," American Journal of Science 261 (December 1, 1963), pages 913–928.

1962

Stephen J. Garland and Anthony W. Knapp, "Algorithm 99: Evaluation of Jacobi symbol," Communications of the ACM 5:6, pages 345–346, June 1962. [PDF]

1959

Stephen J. Garland, "A graphical solution of 3xm game matrices," 1959 Westinghouse Science Talent Search, Mt. Lebanon High School, Mt. Lebanon, Pennsylvania, 1959, 50 pages. [PDF]