next_inactive up previous


Michael J. O'Donnell
(2011 January 27)

$\textstyle \parbox{4.75in}{ \begin{flushleft} The University of Chicago Depa... ...uchicago.edu/\raisebox{-0.25\baselineskip}{\char'176}odonnell} \end{flushleft}}$

$\textstyle \parbox{1.5in}{ \begin{flushleft} 215 Harbor St. Glencoe, IL 60022-1941 (847) 835-1837\\ \emph{michael\_odonnell@acm.org} \end{flushleft}}$




Vita
Birth Spartanburg SC, 4 April, 1952
Family Married, 2 children
Citizenship United States of America




Education
B.S. Computer Sciences Highest Distinction Purdue University 1972
Ph.D. Computer Science R. Constable, advisor Cornell University 1976




Employment
Research Associate University of Toronto 1976-1977
  (on leave from Purdue)  
Assistant Professor Purdue University 1976-1981
Associate Professor Purdue University 1981-1985
Visiting Associate Professor The Johns Hopkins University 1983-1984
  (on leave from Purdue)  
Associate Professor The Johns Hopkins University 1984-1985
  (on leave from Purdue)  
Professor University of Chicago 1985-present
Associate Chairman C.S. University of Chicago 1986-1987
Chairman of C.S. Dept. University of Chicago 1987-1990
Visiting Professor University of Iowa 1996-1997
  (on sabbatical from U. Chicago)  
Senior Fellow University of Chicago 2000-present
in the Computation Institute    




Professional Societies
ACM, IEEE Computer Society, Association for Symbolic Logic, Computer Professionals for Social Responsibility, Acoustical Society of America, American Physical Society, Free Software Foundation, Electronic Frontier Foundation.




Research Interests




Papers in Refereed Journals

Bibliography

1
Geometrical problems with applications to hashing (with D. Comer).
SIAM Journal on Computing, 11(2):217-226, May 1982.
Also appeared as Purdue University Technical Report TR-303, 1979.

2
Pattern matching in trees (with C. Hoffmann).
Journal of the ACM, 29(1):68-95, January 1982.
Also appeared in the collection
Computer Algorithms: string pattern matching strategies,
J.-I. Aoe, editor,
IEEE Computer Society Press, Los Alamitos CA,
1994, 154-181.

3
Programming with equations (with C. Hoffmann).
ACM Transactions on Programming Languages and Systems, 4(1):83-112, January 1982.
A preliminary version of [2,3] with some additional material, appeared as
An interpreter generator using tree pattern matching.
6th Annual ACM Symposium on Principles of Programming Languages, 169-179, January 1979.

4

A critique of the foundations of Hoare-style programming logics.
Communications of the ACM, 25(12):927-934, December 1982.
Also appeared as Purdue University Technical Report TR-338, 1980, and in the
Logics of Programs Workshop, D. Kozen editor, Yorktown Heights, New York, May 1981, Lecture Notes in Computer Science, 131:349-374, Springer-Verlag, 1982.

5
The expressiveness of simple and second order type structures (with S. Fortune and D. Leivant).
Journal of the ACM, 30(1):151-185, January 1983.
Also appeared as IBM Research Report RC 8542 (#37221) 10/31/80.
Some of the material in this paper also appeared in conference [1] and lecture [1].

6
A combinatorial problem concerning interconnection networks (with C. Smith).
IEEE Transactions on Computing, C-31(2):163-164, February 1982.
Also appeared as Purdue University Technical Report CSD TR 352, 1981.

7
A combinatorial analysis of static-key hashing (with F. Berman, M. Bock, E. Dittert and D. Planck).
SIAM Journal on Computing, 15(2):604-618, May 1986.

8
Lower bounds for sorting with realistic instruction sets (with E. Dittert).
IEEE Transactions on Computers, C-34(4):311-317. April 1985.
Also appeared as Johns Hopkins University Technical Report JHU/EECS 84/06.
An error is corrected in C-35(10):932, October 1986.

9
Implementation of an interpreter for abstract equations (with C. Hoffmann and R. Strandh).
Software--Practice and Experience, 15(2):1185-1204, December 1985.
An earlier version, by Hoffmann and O'Donnell, appeared in 10th Annual ACM Symposium on Principles of Programming Languages, 111-120, January 1984.
Also appeared as Johns Hopkins University Technical Report JHU/EECS/84/03, 1984.

10
How to prove representation-independent independence results (with S. Kurtz and J. Royer).
Information Processing Letters, 24:5-10, January 1987.
Also appeared as University of Chicago Department of Computer Science Technical Report 85-006, 1985.

11
Some intuitions behind realizability semantics for constructive logic: Tableaux and Läuchli countermodels (with J. Lipton).
Annals of Pure and Applied Logic, 81:187-239, 1996.

12
Leveled Garbage Collection (with G. Tong).
Journal of Functional and Logic Programming, 2001:5, 2001.

13
Cell-Utes and Flutter-Tongued Cats: Sound Morphing Using Loris and th Reassigned Bandwidth-Enhanced Model (with K. Fitz, L. Haken, S. Lefvert, C. Champion).
Computer Music Journal, 27(3):44-65, Fall 2003.

14
A Proposal to Separate Handles from Names on the Internet.
Communications of the Association for Computing Machinery, 48(12):78-83, December 2005. Longer version in Technical Report [9].




Competitive Conference Papers

Bibliography

1
A programming language theorem which is independent of Peano arithmetic.
11th Annual ACM Symposium on Theory of Computing, 176-186, May 1979.
Similar papers appeared as A practical programming theorem which is independent of Peano arithmetic.
100th Anniversary Conference in honor of Gottlob Frege, Friedrich Schiller Universität, Jena, D.D.R., 1979,
and as Purdue University Technical Report TR-299, 1979.

2
Parallel stepwise simulation of combinatory reduction systems.
1984 Conference on Information Sciences and Systems, Princeton, N.J., May 1984.
A longer version containing additional material appeared as Universal reduction systems for sequential and parallel computation,
Johns Hopkins University Technical Report JHU/EECS/84/04, 1984, and was included in book [3].

3
Realizability semantics for error-tolerant logics (with J. Mitchell).
In J. Halpern, editor, Theoretical Aspects of Reasoning About Knowledge, Proceedings of the 1986 Conference, Morgan Kaufman, New York, 1986.
An earlier version by O'Donnell appeared as A type-theoretic foundation for epistemic and relevance logics, Johns Hopkins University Technical Report JHU/EECS/85/02.

4
Exact real arithmetic: a case study in higher order programming (with H-J. Boehm, R. Cartwright, and M. Riggle).
1987 Symposium on LISP and Functional Programming.

5
Testing confluence of nonterminating overlapping systems of rewrite rules (with Y. Chen).
Conditional and Typed Rewriting Systems,
2nd International CTRS Workshop, Montreal, June 1990. Lecture Notes in Computer Science 516, Springer-Verlag, 1991, pp. 127-136.
Preliminary versions appeared as University of Chicago Department of Computer Science Technical Report 89-03, 1989 and 90-07, 1990.

6
Infinite Terms and Infinite Rewritings (with Y. Chen).
Conditional and Typed Rewriting Systems,
2nd International CTRS Workshop, Montreal, June 1990. Lecture Notes in Computer Science 516, Springer-Verlag, 1991, pp. 115-126.
Preliminary version appeared as University of Chicago Department of Computer Science Technical Report 90-08, 1990.

7
Sound Morphing using Loris and the Reassigned Bandwdith-Enhanced Additive Sound Model: Practice and Applications (with S. Lefvert, K. Fitz, L. Haken). International Computer Music Conference, Göteborg, September 2002.




Book Chapters

Bibliography

1
Introduction: Logic and Logic Programming Languages.
Chapter 1 of Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5 on Logic Programming,
D. Gabbay, editor.
1998, pp. 1-67.

2
Equational Logic Programming.
Chapter 2 of Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5 on Logic Programming,
D. Gabbay, editor.
1998, pp. 69-161.




Open Conference Papers and Technical Reports

Bibliography

1
Toward a fully parallel implementation of the lambda calculus (with R. Strandh).
Johns Hopkins University Technical Report JHU/EECS/84/13, 1984.

2
Multidimensional interpolation at inaccurate points (with E. Dittert).
Johns Hopkins University Technical Report JHU/EECS/84/17, 1984.

3
Proving unorientable equational formulas (with Y. Chen).
University of Chicago Department of Computer Science Technical Report 90-26, August 1990.

4
Nonterminating rewritings with head boundedness (with Y. Chen).
University of Chicago Department of Computer Science Technical Report 90-27, August 1990.

5
Connecting formal semantics to constructive intuitions (with S. Kurtz, J. Mitchell).
Proceedings of a Symposium on Constructivity in Computer Science, Trinity University, San Antonio TX, June 1991.
Lecture Notes in Computer Science, Volume 613, Springer-Verlag, 1992, pp. 1-21.
Also appeared as University of Chicago Department of Computer Science Technical Report 92-01, January 1992.
Also presented at the annual meeting of the Association for Symbolic Logic, Notre Dame, February 1993.

6
Decomposition of steady state instrument data into an excitation system and formant filter components (with I. Bisnovatyi).
COST Digital Audio Effects Workshop, DAFx99, Trondheim, Norway, 9-11 December 1999, pp. 113-116.

7
The Sound Manifesto (with I. Bisnovatyi).
Critical Technologies for the Future of Computing,
The International Society for Optical Engineering (SPIE), San Diego, CA, 30 July through 4 August 2000.

8
Open Network Handles Implemented in DNS.
Internet Draft draft-odonnell-onhs-imp-dns-00.txt filed with Internet Engineering Task Force, 17 September 2002. A version with different pagination is archived permanently in the Computing Research Repository (CoRR, http://xxx.lanl.gov/archive/cs/intro.html) as cs.NI/0301011, 14 January 2003.

9
A Proposal to Separate Handles from Names on the Internet.
Computing Research Repository (CoRR, http://xxx.lanl.gov/archive/cs/intro.html), number cs.NI/0302017, 12 February 2003. Shorter version in Refereed [14].




In Preparation and Submitted

Bibliography

1
Against Nonmonotonic Logic.

2
Relational realizability (with J. Lipton).




Books

Bibliography

1
Computing in Systems Described by Equations, Lecture Notes in Computer Science, Volume 58, Springer-Verlag, 1977.
A preliminary version appeared as Subtree replacement systems: a unifying theory for recursive equations, LISP, Lucid and combinatory logic.
9th Annual ACM Symposium on Theory of Computing, 295-305, May 1977.
Also appeared as Reduction Strategies in Subtree Replacement Systems, Ph.D. Dissertation, Cornell University, August 1976.

2
A Programming Logic (with R. Constable), Winthrop, 1978.

3
Equational Logic as a Programming Language, MIT Press, 1985.
Includes some material from papers [2,3,9] and conference [2], as well as original material.




Software Research Projects

Equation Interpreter/Compiler, (with C. Hoffmann, G. Sacco, P. Golick, R. Strandh, S. Rebelsky, D. Sherman, S. Bailey). Announced in SIGPLAN Notices, September 1983. Demonstrated at the Workshop on Logics of Programs, 1985. Abstract appeared as ``Equational logic as a programming language'', Logics of Programs: Proceedings 1985, Lecture Notes in Computer Science 193:255, Springer-Verlag, 1985. First distribution May, 1983. Second distribution as compiler December, 1985. Distributed to Purdue University; Indiana University; The Johns Hopkins University; Los Alamos National Laboratory; Stichting Mathematisch Centrum, Amsterdam; Oregon Graduate Center; Universität des Saarlandes; Mergenthaler Linotype, Frankfurt; Philips Research Laboratories, Sunnyvale, California; University of North Carolina; Moorhead State University; Tektronix, Portland, Oregon; The Foxboro Co., Massachusetts; Colby College; Scientific Calculations, Inc., Santa Cruz, California; University of Iowa; Telefonaktiebolaget L. M. Ericsson, Stockholm, Sweden; Universität Ulm, Germany; U.C. Berkeley; SUN Microsystems; SCS, Hamburg; University of Michigan; Lulea University, Sweden; University of Tasmania; University of York; University of Wisconsin; Advanced Computer Communications, Santa Barbara, CA; MCC; Franz, Inc.; Université de Genève; Rice University; University of Louvain; University of North Carolina; University of Washington; University of Arizona; Software Research Associates, Tokyo; Weizmann Institute; SUNY College of Technology; Imperial Software Technology, Cambridge England; Collège Militaire Royal de Saint-Jean, Quebec; Gesselschaft für Mathematik und Datenverarbeitung mbH, Sankt Augustin, Germany; MacQuarie University, North Ryde, Australia; University of Nebraska; Memorial University of Newfoundland; Universität Kaiserslautern; Carnegie-Mellon University; University of Queensland, Australia; University of New Hampshire.

LATEX macros for the Chicago Journal of Theoretical Computer Science. cjstruct.cls allows unambiguous structural markup of published journal articles in LATEX source format. First version distributed 4 April 1995. Used by MIT Press for CJTCS and for the Journal of Functional and Logic Programming.




Invited Lectures

Bibliography

1
Computational complexity and proof-theoretic power in typed lambda calculi.
American Mathematical Society Summer Meeting, 1982.
Abstract appeared in Abstracts of the American Mathematical Society, 3(5):376, August 1982.
Results from paper [5].

2
Two lectures on logic and computer science: 1. Does arrow denote implication or functionality? A profound mathematical pun. 2. Why the Church-Turing thesis doesn't help parallel functional programming.
University of Maryland Special Year in Mathematical Logic and Theoretical Computer Science, October 1984.
Results from paper [5], book [3], and original material.

3
What it means to have a universal parallel reduction language.
Graph Reduction Workshop, Santa Fe, October 1986.
Results from book [3].

4
Survey of the equational logic programming project.
Colloquium on Resolution of Equations in Algebraic Structures, Lakeway, Texas, March 1987.
Survey of material from papers [3,9], book [3], plus original material.

5
Term-rewriting implementation of equational logic programming.
In P. Lescanne, editor, Rewriting Techniques and Applications -- Bordeaux, France, May 1987 -- Proceedings, Lecture Notes in Computer Science, 256, Springer-Verlag, 1987.
Similar material to invited lecture [4].

6
Open Problems in Equational Logic Programming.
Distinguished Lecture Series, SUNY Stony Brook, February 1988.
Similar material to invited lectures [4,5].

7
Equational Logic as a Programming Language.
Colloquium Series in Term Rewriting, Portland State University, March 1991.
Similar material to invited lectures [4,5,6].

8
Electronic Journals--scholarly invariants in a changing medium.
Conference on Academic and Professional Journals in the Twentieth Century, University of Chicago, April 1992 (presented by author as discussant for session on ``The Future of Journals'').
Also appeared (invited, unrefereed) in Journal of Scholarly Publishing, volume 26, number 3, April 1995, University of Toronto Press, pp. 183-199, and as University of Chicago Department of Computer Science Technical Report 92-07, April 1992.

9
Issues Involved in Publishing an Electronic Journal.
Seminars on Academic Computing 1993 University Executive Program, Snowmass CO, August 1993.
Very similar to [8], but a more detailed presentation--revised version of paper appeared as University of Chicago Department of Computer Science Technical Report 93-11, July 1993.

10
Intuitive Counterexamples for Constructive Fallacies (with J. Lipton).
Mathematical Foundations of Computer Science 1994 -- 19th International Symposium, MFCS '94, Kosice, Slovakia, August 1994 -- Proceedings, Lecture Notes in Computer Science, volume 841, Igor Prívara, Branislav Rovan and Peter Ruzicka editors, Springer-Verlag, 1994, pp. 87-111.

11
The Structure of Scholarship in Cyberspace.
Professors and Publishing in the Electronic Academy. The University of Tennessee, Knoxville Library, September 1996.

12
The Sources of Certainty in Computation and Formal Systems.
Computer Science as a Human Science: The Cultural Impact of Computerization, the 1999-2000 Sawyer Seminar at the University of Chicago. The University of Chicago, October 1999.

13
Against Nonmonotonic Logic. ACM SIGART Chicago, March 2001.




Editorial Duties
  1. Category editor for Theory of Computation, Computing Reviews, 1985-1987.
  2. Managing Editor and founder of the Chicago Journal of Theoretical Computer Science, a refereed scholarly journal published by MIT Press on the World Wide Web, 1994-2000.
  3. Editorial Board for the Journal of Functional and Logic Programming, 1995-present.
  4. Advisory Board for Logical Methods in Computer Science, 2002-present.
  5. Moderator for the Sound topic in the CoRR online repository of technical reports, 2002-present.




Refereeing
Journal of Computer and Systems Sciences; SIAM Journal on Computing; Communications of the ACM; Journal of the ACM; ACM Transactions on Programming Languages and Systems; Information Processing Letters; Software Practice and Experience; Journal of Computer Languages; Theoretical Computer Science; Information and Control; Acta Informatica; Journal of Philosophical Logic. ACM annual conference; MIT Press; Elsevier North-Holland; Springer-Verlag; National Science Foundation; Research Council of Canada; Australian Research Grants Scheme; Journal of Symbolic Computation.




Program Committees
  1. 25th Annual IEEE Symposium on the Foundations of Computer Science, 1984.
  2. 12th Annual ACM Symposium on Principles of Programming Languages, 1985.
  3. 26th Annual IEEE Symposium on the Foundations of Computer Science, 1985.
  4. 1985 Conference on Information Sciences and Systems, cochairman.
  5. 13th Annual ACM Symposium on Principles of Programming Languages, 1986
  6. 14th Annual ACM Symposium on Principles of Programming Languages, 1987, chairman.
  7. Rewriting Techniques and Applications, 1991.
  8. Rewriting Techniques and Applications, 1993.
  9. Dartmouth Institute for Advanced Graduate Studies, 4th annual summer symposium, Electronic Publishing and the Information Superhighway, 1995.
  10. Algebraic Methodology and Software Technology, 2000.




Professional Service
  1. Organized Midwest Theory of Computation Meeting, December 1986.
  2. Founder and president of Midwest Society for Programming Languages and Systems (Midwest Local SIGPLAN), 1987-1994.
  3. National Science Foundation Research Initiation Panel, February 1988.
  4. Conference cochair for 16th Annual ACM Symposium on Principles of Programming Languages, 1989.
  5. Advisory Board for Foundations of Computation Laboratory, Key Centre for Software Technology, Department of Computer Science, The University of Queensland, 1989-present.
  6. National Science Foundation Small-Scale Institutional Infrastructure Panel, June 1990.
  7. Founded the Association of Electronic Scholarly Journals, 1990.
  8. New York Statewide Review of Doctoral Programs, site visitor, October 1990.
  9. Universities Space Research Association Science Councils: CESDIS 1991-1996, ICASE 1991-1992.
  10. Conference cochair for research contributions Constructivity in Computer Science, 1991.
  11. NSF/CRA Workshop on the Computing Research Infrastructure, July 1991.
  12. Advisory Board for the Information Science Research Institute at the University of Nevada, Las Vegas, 1991-1994.
  13. Organizing Committee, Third International Conference on Algebraic Methodology and Software Technology, 1992-1993.
  14. Organized Annual NSF Infrastructure Workshop, June 1993.
  15. Chair of ACM SIGSOUND, 2001-2003.




University Administration and Service
Purdue University

The Johns Hopkins University
The University of Chicago




Community Service




Research Grants and Contracts
  1. A Uniform Theory for Implementations of Descriptive Languages (with C. Hoffmann $5,400) Purdue Summer XL grant, 1978.
  2. A Uniform Theory for Implementations of Descriptive Languages (with C. Hoffmann $71,117) National Science Foundation, 1978-1980.
  3. A Uniform Theory for Implementations of Descriptive Languages (with C. Hoffmann $160,659) National Science Foundation, 1981-1983.
  4. Research on Programming with Equations (with C. Hoffmann $116,149) National Science Foundation, 1983-1985.
  5. Highly Parallel Architectures for General-Purpose Concurrent Programming Languages (with G. Masson $57,940) National Security Agency, 1984-1985.
  6. Equational Logic as a Programming Language ($27,500) Louis Block Fund, 1985-1986.
  7. Equational Logic as a Programming Language ($185,193) National Science Foundation, 1986-1988.
  8. Theory and Implementation of Equational Logic Programming ($176,333) National Science Foundation, 1988-1990.
  9. The University of Chicago Computer Science Laboratory ($2,030,221) National Science Foundation, 1989-1994.
  10. Rigorous Mathematical Sciences Curriculum for the Humanities and Social Sciences ($50,000) National Science Foundation 1990-1992.
  11. Theory and Implementation of Equational Logic Programming ($161,136) National Science Foundation, 1991-1993.




Meetings Attended
  1. 17th Annual Symposium on Foundations of Computer Science, Houston, 1976.
  2. 9th Annual Symposium on Theory of Computing, Boulder, 1977.
  3. 19th Annual Symposium on Foundations of Computer Science, Ann Arbor, 1978.
  4. 6th Annual Symposium on Principles of Programming Languages, San Antonio, 1979.
  5. 11th Annual Symposium on Theory of Computing, Atlanta, 1979.
  6. Frege Conference, Friedrich Schiller Universität, Jena, DDR, 1979.
  7. 12th Annual Symposium on Theory of Computing, Los Angeles, 1980.
  8. 21st Annual Symposium on Foundations of Computer Science, Syracuse, 1980.
  9. Verification Workshop, Yorktown Heights, NY, 1981.
  10. 13th Annual Symposium on Theory of Computing, Milwaukee, 1981.
  11. Workshop on Recursion Theoretic Aspects of Computer Science, W. Lafayette IN, 1981.
  12. 14th Annual Symposium on Theory of Computing, San Francisco, 1982.
  13. 23rd Annual Symposium on Foundations of Computer Science, Chicago, 1982.
  14. 15th Annual Symposium on Theory of Computing, Boston, 1983.
  15. 24th Annual Symposium on Foundations of Computer Science, Tucson, 1983.
  16. Brooklyn College Symposium on Theoretical Computer Science I: Logic in Computer Science, 1983.
  17. 11th Annual Symposium on Principles of Programming Languages, Salt Lake City, 1984.
  18. International Symposium on Logic Programming, Atlantic City, 1984.
  19. 1984 Conference on Information Sciences and Systems, Princeton NJ.
  20. 16th Annual Symposium on Theory of Computing, Washington DC, 1984.
  21. 25th Annual Symposium on Foundations of Computer Science, West Palm Beach, 1984.
  22. University of Maryland Special Year in Mathematical Logic and Theoretical Computer Science, 1984-1985.
  23. 12th Annual Symposium on Principles of Programming Languages, New Orleans, 1985.
  24. Logics of Programs Workshop, Brooklyn New York, 1985.
  25. 26th Annual Symposium on Foundations of Computer Science, Portland OR, 1985.
  26. 13th Annual Symposium on Principles of Programming Languages, St. Petersburg FL, 1986.
  27. Workshop on Theoretical Aspects of Reasoning About Knowledge, Asilomar CA, 1986.
  28. SIGPLAN 1986 Symposium on Practical Program Development Environments, Palo Alto CA.
  29. 14th Annual Symposium on Principles of Programming Languages, Munich, 1987.
  30. Colloquium on Resolution of Equations in Algebraic Structures, Lakeway, Texas, 1987.
  31. 2nd International Conference on Rewriting Techniques and Applications, Bordeaux, 1987.
  32. SIGPLAN 1987 Symposium on Interpreters and Interpretive Techniques, St. Paul MN.
  33. 15th Annual Symposium on Principles of Programming Languages, San Diego CA, 1988.
  34. 1988 Snowbird Meeting of CS and EECS Department Chairs, Snowbird UT.
  35. National Computer Conference, Louisville KY, 1988.
  36. 16th Annual Symposium on Principles of Programming Languages, Austin TX, 1989.
  37. 3rd International Conference on Rewriting Techniques and Applications, Chapel Hill NC, 1989.
  38. 17th Annual Symposium on Principles of Programming Languaes, San Francisco CA, 1990.
  39. 1990 CER/II Meeting, Atlanta GA, 1990.
  40. Association of Research Libraries Meeting about Refereed Academic Electronic Publishing Projects, Raleigh NC, 1990.
  41. Symposium on Constructivity in Computer Science, San Antonio TX, 1991.
  42. NSF/CRA Workshop on the Computing Research Infrastructure, Washington DC, 1991.
  43. 19th Annual Symposium on Principles of Programming Languages, Albuquerque NM, 1992.
  44. Symposium on Character Recognition and Document Analysis, Las Vegas NV, 1992.
  45. Conference on Academic and Professional Journals in the Twentieth Century, Chicago IL, 1992.
  46. Association for Symbolic Logic, Annual Meeting, South Bend IN, 1993.
  47. Annual NSF Infrastructure Workshop, 1993.
  48. 8th Annual IEEE Symposium on Logic in Computer Science, Montreal Québec, 1993.
  49. Seminars on Academic Computing, University Executive Program, 1993.
  50. International Conference on Refereed Electronic Journals, Winnipeg Manitoba, 1993.
  51. Mathematical Foundations of Computer Science 1994 -- 19th International Symposium, Kosice, Slovakia, 1994
  52. Acoustical Society of America, Indianapolis, 1996.
  53. Professors and Publishing in the Electronic Academy. The University of Tennessee, Knoxville Library, 1996.
  54. Acoustical Society of America, Seattle, 1998.
  55. COST Digital Audio Effects Workshop (DAFx99)), Trondheim, Norway, 1999.
  56. Acoustical Society of America, Chicago, 2001.
  57. National Science Foundation Summit on Future Internet Architecture, Arlington VA, October 12-15 2009 (by invitation).




Unrefereed Lectures
  1. Rigorous Development of a Lucid Interpreter. University of Waterloo, Fall 1976.
  2. Automatic Interpreter Generation. Indiana University, Fall 1978; SUNY Buffalo, 16 February, 1979; IBM Research, Yorktown Hts., 8 March, 1979; IBM Research San Jose, 12 March, 1979; M.I.T., 9 April, 1979; Technische Universität, W. Berlin, 14 May, 1979; Universität Aachen, 30 May, 1979; Munich Universität, 31 May, 1979.
  3. A Programming Language Theorem Which is Independent of Peano Arithmetic. Cornell University, August, 1978; SUNY Buffalo, 15 February, 1979; Universität Bielefeld, 16 May, 1979; Universität Kiel, 18 May, 1979; Universität Heidelberg, 22 May, 1979; Universität Münster, 25 May, 1979; Mathematical Institute, Warsaw, 4 June, 1979; Mathematical Institute, Amsterdam, 6 June, 1979.
  4. Logic For Reasoning About Programs. Purdue University, April 1977; Humboldt Universität, E. Berlin, 15 May, 1979.
  5. A Critique of the Foundations of Hoare-Style Programming Logics. New Mexico State University, 23 September, 1980 (videotape sent to University of New Mexico, New Mexico Tech.); Los Alamos Laboratories, 24 September, 1980; Verification Workshop, IBM Research Yorktown Heights, 5 May, 1981.
  6. The Intuitive Foundations of Programming Logic. New Mexico Tech., 22 September, 1980; Los Alamos Laboratories, 24 September, 1980.
  7. Implementation of an Interpreter for Abstract Equations. Iowa State University, 18 November, 1982; University of Maryland, 5 April, 1983; The Johns Hopkins University, 30 March, 1983; Cornell University, 3 August, 1983; New Mexico State University, 10 November, 1983; University of North Carolina, 19 March, 1984; AT&T Bell Laboratories, Murray Hill, 28 August, 1984; University of Connecticut, 16 November, 1984.
  8. Equational Logic as a Programming Language. Tektronix, 4 February, 1985; University of Washington, 5 February, 1985; IBM Research, Yorktown Heights, 22 February, 1985; University of Delaware, 4 March, 1985; University of Wisconsin, 14 March, 1985; AT&T Bell Laboratories, Murray Hill, 21 March, 1985; Carnegie-Mellon University, 23 September, 1985; University of Pennsylvania, 26 September, 1985; Xerox PARC, 18 March, 1986; DePaul University, 1986; Mathematisch Centrum, Amsterdam, 15 January, 1987, Technische Universität, Berlin, 19 January, 1987; GMD Karlsruhe, Germany, 20 May, 1987; INRIA Sophia-Antipolis, France, 22 May, 1987.
  9. Lower Bounds for Sorting With Realistic Instruction Sets. University of Chicago, 7 February, 1985.
  10. Fault-Tolerant Logic for Automated Reasoning. SUNY Stony Brook, 20 February, 1985; University of Amsterdam, 16 January, 1987.
  11. Semantics for Infinite and Indeterminate Computations in Logic Programming Languages. Midwest Theory of Computation Meeting, Purdue, 19 April, 1986.
  12. Intuitive Constructive Semantics for Constructive Logic. Midwest Theory of Computation Meeting, University of Illinois, 15 April, 1987.
  13. A Compiler for Equational Logic Programs. Midwest Society for Programming Languages and Systems, University of Illinois, Spring, 1988.
  14. Open Problems in Equational Logic Programming. The Johns Hopkins University, 3 December, 1987; DePaul University, 29 January, 1988; SUNY Stony Brook, 26 February, 1988; University of Illinois at Chicago, 3 October, 1988; Indiana University at South Bend, December 6, 1989; University of Nevada at Las Vegas, 16 January, 1990; Universität Dortmund, 12 November, 1990; Universität Kaiserslautern, 14 November, 1990; Universität Ulm, 15 november, 1990; OCATE, Portland OR, 26 March, 1991.
  15. Meaningful Semantics for Constructive Logic. University of Maryland, 2 May, 1990; Universität Würzburg, 10 November, 1990.
  16. Connecting Formal Semantics to Constructive Intuitions. Midwest Theory of Computation Meeting, Northwestern University, 6 December, 1992; ASL Annual Meeting, Notre Dame University, 12 March, 1993; Université Pau 26 March, 1993; Université Bordeaux, 22 March and 1 April, 1993; Cornell University 7 June, 1993; Wesleyan University, 20 September 1993.
  17. Applications of Logic to Programming Language Design and Implementation. The Johns Hopkins University, 17 December, 1992.
  18. Term Tours--I/O for Lazy Functional Programs (work of Samuel Rebelsky as my Ph.D. Student). Universität Kaiserslautern, 18 February, 1993; Max Planck Institut, Saarbrucken, 18 February, 1993; Williams College, 24 September 1993, Grinnell College, 18 November 1993.
  19. Electronic Publication, Refereeing, and the Economy of Attention. University of Chicago, Physics Department, 7 October, 1993.
  20. Intuitive Counterexamples for Constructive Fallacies. SUNY Buffalo, 7 October 1994.
  21. Electronic Journals -- scholarly invariants in a changing medium. SUNY Buffalo, 7 October 1994; Dartmouth, 26 October 1994.
  22. Digital Sound Synthesis. Wesleyan University, 25 October 1994; Dartmouth, 26 October 1994; Carleton College, 30 January 1996.
  23. Program Execution as Logical Deduction. Macalester College, 31 January 1996.
  24. Leveled Garbage Collection. The University of Iowa, 13 April 1998.
  25. Minimal public-key infrastructure. USTC Hefei, 2000.
  26. Why is P$\neq$NP so Hard to Prove? Chinese Academy of Science, Beijing, 11 September 2003.
  27. Prediction vs. Commitment in Garbage Collection. USTC Hefei, September 18 2003.
  28. Minimal public-key infrastructure. Wesleyan University, November 15 2004.
  29. The relevance of relevance. Universidad Complutense de Madrid, June 12 2006.
  30. End-to-end public-key infrastructure. Universidad Politecnicá de Madrid, July 5 2006.
  31. Time-frequency analysis. Reed College Math Colloquium, September 9 2010.
  32. The sources of certainty in computation and formal systems, University of Chicago Formal Philosophy Workshop, November 23 2010.




Consulting and Visiting




M.S. Students
  1. The University of Chicago
    1. Susanne Lefvert (visiting from Lulea University of Technology), 2001-2002, user interface for Loris sound synthesis/morphing/analysis.




Ph.D. Students
  1. Purdue University
    1. Paul Chew, 1979-1981, Normal Forms in Term Rewriting Systems.
    2. Eric Dittert, 1980-1982, On the Complexity of Retrieving Information.
  2. The Johns Hopkins University
    1. Robert Strandh, 1983-1987, Compiling Equational Programs into Efficient Machine Code.
  3. The University of Chicago
    1. Samuel Rebelsky, 1987-1993, Tours, a System for Lazy Term-Based Communication.
    2. David Sherman, 1987-1994, Run-Time and Compile-Time Improvements to Equational Programs.
    3. Donald Ziff, 1989-1995, Lazy Functional Programming for Full-Text Information Retrieval.
    4. Stephen Bailey, 1988-1995, Hielp, a Fast Interactive Lazy Functional Language System.
    5. Guanshan Tong, 1993-1997, Design and Evaluation of a High-Performance Automatic Memory Management System.
    6. Ilya Bisnovatyi, 1993-2006 (withdrew), sound synthesis.




Postdoctoral Associates
  1. William Winsborough, 1988-90.
  2. Yiyun Chen, 1989-91.




Courses Taught

Summary

Undergraduate

Graduate

Chronology (G-graduate, U-undergraduate)

Cornell University
Spring 1976 CS 790 Seminar in Program Verification (G)
University of Toronto
Spring 1977 CSC 336S Numerical Analysis (U)
Purdue University
Autumn 1977 CS 220N Programming I (U)
    CS 484 Theory of Computation (U)
    CS 590V Seminar in Programming Logic (G)
Spring 1978 CS 484 Theory of Computation (U)
    CS 482 Algorithm Design and Analysis (U)
Autumn 1978 CS 230 Programming I (U)
    CS 484 Theory of Computation (U)
Spring 1979 CS 330 Programming II (U)
    CS 582 Survey of Algorithms, Automata, and Formal Languages (G)
Autumn 1979 CS 430 Data Structures (U)
    CS 582 Survey of Algorithms, Automata, and Formal Languages (G)
Spring 1980 CS 580 Algorithm Design and Implementation (G)
    CS 590B Seminar in Programming Logic and Verification (G)
Autumn 1980 CS 320 Programming II for Engineers and Scientists (U)
    CS 582 Survey of Algorithms, Automata, and Formal Languages (G)
Spring 1981 CS 540 File Structures (G)
    CS 584 Theory of Algorithms and Computational Complexity (G)
Autumn 1981 CS 540 File Structures (G)
Spring 1982 CS 580 Algorithm Design and Implementation (G)
Autumn 1982 CS 414 Numerical Methods (U)
    CS 484 Introduction to the Theory of Computation (U)
Spring 1983 CS 584 Theory of Algorithms and Computational Complexity (G)
The Johns Hopkins University
Autumn 1983 52.329 Logic Programming (G)
Spring 1984 52.324 The Lambda Calculus and Its Relationship
    With Computable Functions (G)
Autumn 1984 52.8 Introduction to Computer Programming (U)
Spring 1985 52.8 Introduction to Computer Programming (U)

The University of Chicago
Winter 1986 Constructive Logic Seminar (G)
Winter-Spring 1986 ComSci 388 Logic Programming Languages I-II (G)
Winter-Spring 1987 ComSci 488 The Lambda Calculus (G)
Winter-Spring 1988 ComSci 388 Logic Programming Languages I-II (G)
Autumn 1988 ComSci 280 Theory of Computation I (U)
Winter 1989 ComSci 221 Programming Languages (U)
Winter 1990 ComSci 221 Programming Languages (U)
Spring 1990 ComSci 388 Equational Logic Programming (G)
Autumn 1990 ComSci 280 Theory of Computation I (U)
Winter 1991 ComSci 221 Programming Languages (U)
Autumn 1991 ComSci 319 The Lambda Calculus (G)
Winter 1992 ComSci 221 Programming Languages (U)
Spring 1992 ComSci 281 Theory of Computation II (U)
Autumn 1992 ComSci 388 Logic Programming Languages (G)
Winter 1993 ComSci 221 Programming Languages (U)
Autumn 1993 ComSci 398 Seminar on Sound Modeling (G)
Winter 1994 ComSci 221 Programming Languages (U)
Winter 1994 ComSci 398 Seminar on Sound Modeling (G)
Spring 1994 ComSci 295 Digital Sound Modeling (U)
Winter 1995 ComSci 221 Programming Languages (U)
Spring 1995 ComSci 295 Digital Sound Modeling (U)
Autumn 1995 ComSci 230/330 Operating Systems (U/G)
Winter 1996 ComSci 231/331 Advanced Operating Systems (U/G)
Spring 1996 ComSci 295 Digital Sound Modeling (U)

The University of Iowa
Spring 1997 22C:096 Computation Information & Description (U)
Spring 1997 22C:196 Digital Sound Modeling (U)

The University of Chicago
Autumn 1997 ComSci 501 System Administration in Linux (G)
Winter 1998 ComSci 222/322 Machine Organization (U/G)
Spring 1998 ComSci 230/330 Operating Systems (U/G)
Autumn 1998 ComSci 105 Fundamentals of Computer Programming (U)
Winter 1999 ComSci 222/322 Computer Architecture (U/G)
Spring 1999 ComSci 295 Digital Sound Modeling (U)
Autumn 1999 ComSci 221/321 Programming Languages (U/G)
Winter 2000 ComSci 319 The Lambda Calculus (G)
Spring 2000 ComSci 295 Digital Sound Modeling (U)
Autumn 2000 ComSci 221 Programming Languages (U)
Winter 2001 ComSci 392 Realizability Semantics (G)
Spring 2001 ComSci 295 Digital Sound Modeling (U)
Autumn 2001 ComSci 22100 Programming Languages (U)
Spring 2002 ComSci 31900 Lambda Calculus (G)
Spring 2002 ComSci 29500 Digital Sound Modeling (U)
Autumn 2002 ComSci 12500 Honors Introduction to Computer Programming (U)
Autumn 2002 ComSci 22800 Free Software Practicum (U)
Spring 2003 ComSci 22800 Free Software Practicum (U)
Spring 2003 ComSci 29500 Digital Sound Modeling (U)
Autumn 2003 CMSC 16100 Honors Introduction to Computer Programming (U)
Spring 2004 CMSC 29500 Digital Sound Modeling (U)
Winter 2005 CMSC 34910 Mathematical Transforms for Signal Processing (G)
Spring 2005 CMSC 29500 Digital Sound Modeling (U)
Spring 2005 CMSC 31900 Lambda Calculus (G)
Autumn 2006 CMSC 31100 Big Ideas in Computer Science (G)
Winter 2007 CMSC 29500 Digital Sound Modeling (U)
Spring 2007 CMSC 33601 Strategic Choices in Designing the Internet (G))
Autumn 2008 CMSC 31100 Big Ideas in Computer Science (G)
Winter 2008 CMSC 29500 Digital Sound Modeling (U)
Spring 2009 CMSC 33601 Strategic Choices in Designing the Internet (G))
Autumn 2009 CMSC 31100 Big Ideas in Computer Science (G)
Spring 2010 CMSC 29500 Digital Sound Modeling (U)
Autumn 2010 CMSC 31100 Big Ideas in Computer Science (G)

About this document ...

This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.71)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html -split 0 vitae.tex

The translation was initiated by Mike O'Donnell on 2011-01-27

next_inactive up previous
Mike O'Donnell 2011-01-27