Michael J. O'Donnell
(2011 January 27)
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 
19761977 

(on
leave from Purdue) 

Assistant Professor 
Purdue University 
19761981 
Associate Professor 
Purdue University 
19811985 
Visiting Associate Professor 
The Johns Hopkins University 
19831984 

(on leave from Purdue) 

Associate Professor 
The Johns Hopkins University 
19841985 

(on leave from
Purdue) 

Professor 
University of Chicago 
1985present 
Associate Chairman C.S. 
University of Chicago 
19861987 
Chairman of C.S. Dept. 
University of Chicago 
19871990 
Visiting Professor 
University of Iowa 
19961997 

(on
sabbatical from U. Chicago) 

Senior Fellow 
University of Chicago 
2000present 
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
 Infrastructure for public key distribution.
 The nature of formal systems.
 Sound synthesis.
 Semantics for constructive reasoning.
Papers in Refereed Journals
 1
 Geometrical problems with applications to hashing
(with D. Comer).
SIAM Journal on Computing,
11(2):217226, May 1982.
Also appeared as Purdue
University Technical Report TR303, 1979.
 2
 Pattern matching in trees (with C. Hoffmann).
Journal of the ACM, 29(1):6895, 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, 154181.
 3
 Programming with equations (with C. Hoffmann).
ACM Transactions on Programming Languages and
Systems, 4(1):83112, 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, 169179, January 1979.
 4

A critique of the foundations of
Hoarestyle programming logics.
Communications of
the ACM, 25(12):927934, December 1982.
Also appeared
as Purdue University Technical Report TR338, 1980, and in the
Logics of Programs Workshop, D. Kozen editor,
Yorktown Heights, New York, May 1981, Lecture Notes in Computer
Science, 131:349374, SpringerVerlag, 1982.
 5
 The expressiveness of simple and second order type
structures (with S. Fortune and D. Leivant).
Journal
of the ACM, 30(1):151185, 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, C31(2):163164, February 1982.
Also appeared as Purdue University Technical Report CSD TR
352, 1981.
 7
 A combinatorial analysis of statickey hashing (with
F. Berman, M. Bock, E. Dittert and D. Planck).
SIAM
Journal on Computing, 15(2):604618, May 1986.
 8
 Lower bounds for sorting with realistic instruction
sets (with E. Dittert).
IEEE Transactions on
Computers, C34(4):311317. April 1985.
Also
appeared as Johns Hopkins University Technical Report JHU/EECS
84/06.
An error is corrected in C35(10):932, October
1986.
 9
 Implementation of an interpreter for abstract
equations (with C. Hoffmann and R. Strandh).
SoftwarePractice and Experience, 15(2):11851204, December
1985.
An earlier version, by Hoffmann and O'Donnell,
appeared in 10th Annual ACM Symposium on Principles of
Programming Languages, 111120, January 1984.
Also
appeared as Johns Hopkins University Technical Report
JHU/EECS/84/03, 1984.
 10
 How to prove representationindependent
independence results (with S. Kurtz and J. Royer).
Information Processing Letters, 24:510, January 1987.
Also appeared as University of Chicago Department of
Computer Science Technical Report 85006, 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:187239, 1996.
 12
 Leveled Garbage Collection (with
G. Tong).
Journal of Functional and Logic
Programming, 2001:5, 2001.
 13
 CellUtes and FlutterTongued Cats: Sound
Morphing Using Loris and th Reassigned BandwidthEnhanced Model (with
K. Fitz, L. Haken, S. Lefvert, C. Champion).
Computer
Music Journal, 27(3):4465, Fall 2003.
 14
 A Proposal to Separate Handles from
Names on the Internet.
Communications of the
Association for Computing Machinery, 48(12):7883, December
2005. Longer version in Technical Report [9].
Competitive Conference Papers

 1
 A programming language theorem which is
independent of Peano arithmetic.
11th Annual ACM
Symposium on Theory of Computing, 176186, 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 TR299, 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 errortolerant 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 typetheoretic
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 HJ. 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, SpringerVerlag, 1991, pp.
127136.
Preliminary versions appeared as University of
Chicago Department of Computer Science Technical Report 8903, 1989
and 9007, 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, SpringerVerlag, 1991,
pp. 115126.
Preliminary version appeared as University
of Chicago Department of Computer Science Technical Report 9008,
1990.
 7
 Sound Morphing using Loris and the Reassigned
BandwdithEnhanced Additive Sound Model: Practice and Applications
(with S. Lefvert, K. Fitz, L. Haken). International Computer
Music Conference, Göteborg, September 2002.
Book Chapters

 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. 167.
 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. 69161.
Open Conference Papers and Technical Reports

 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 9026, August 1990.
 4
 Nonterminating rewritings with head boundedness
(with Y. Chen).
University of Chicago Department of
Computer Science Technical Report 9027, 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, SpringerVerlag,
1992, pp. 121.
Also appeared as University of Chicago
Department of Computer Science Technical Report 9201, 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, 911 December 1999, pp. 113116.
 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 draftodonnellonhsimpdns00.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

 1
 Against Nonmonotonic Logic.
 2
 Relational realizability (with
J. Lipton).
Books

 1
 Computing in Systems Described by Equations,
Lecture Notes in Computer Science, Volume 58, SpringerVerlag,
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, 295305, 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, SpringerVerlag, 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 SaintJean, 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; CarnegieMellon
University; University of Queensland, Australia; University of New
Hampshire.
L^{A}TEX macros for the Chicago Journal of Theoretical Computer
Science. cjstruct.cls allows unambiguous
structural markup of published journal articles in L^{A}TEX 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

 1
 Computational complexity and prooftheoretic 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 ChurchTuring 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
 Termrewriting implementation of equational logic
programming.
In P. Lescanne, editor, Rewriting
Techniques and Applications  Bordeaux, France, May 1987 
Proceedings, Lecture Notes in Computer Science, 256,
SpringerVerlag, 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 Journalsscholarly
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. 183199, and as
University of Chicago Department of Computer Science Technical
Report 9207, 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
presentationrevised version of paper appeared as University of
Chicago Department of Computer Science Technical Report 9311, 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, SpringerVerlag, 1994, pp.
87111.
 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 19992000 Sawyer
Seminar at the University of Chicago. The University of Chicago,
October 1999.
 13
 Against Nonmonotonic
Logic. ACM SIGART Chicago, March 2001.
Editorial Duties
 Category editor for Theory of Computation, Computing
Reviews, 19851987.
 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, 19942000.
 Editorial Board for the Journal of Functional and
Logic Programming, 1995present.
 Advisory Board for Logical Methods in Computer Science, 2002present.
 Moderator for the Sound topic in the CoRR online
repository of technical reports, 2002present.
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 NorthHolland; SpringerVerlag;
National Science Foundation; Research Council of Canada; Australian
Research Grants Scheme; Journal of Symbolic Computation.
Program Committees
 25th Annual IEEE Symposium on the Foundations of Computer
Science, 1984.
 12th Annual ACM Symposium on Principles of Programming
Languages, 1985.
 26th Annual IEEE Symposium on the Foundations of Computer
Science, 1985.
 1985 Conference on Information Sciences and Systems,
cochairman.
 13th Annual ACM Symposium on Principles of Programming
Languages, 1986
 14th Annual ACM Symposium on Principles of Programming
Languages, 1987, chairman.
 Rewriting Techniques and Applications, 1991.
 Rewriting Techniques and Applications, 1993.
 Dartmouth Institute for Advanced Graduate Studies, 4th
annual summer symposium, Electronic Publishing and the Information
Superhighway, 1995.
 Algebraic Methodology and Software Technology, 2000.
Professional Service
 Organized Midwest Theory of Computation Meeting, December 1986.
 Founder and president of Midwest Society for Programming
Languages and Systems (Midwest Local SIGPLAN), 19871994.
 National Science Foundation Research Initiation Panel, February
1988.
 Conference cochair for 16th Annual ACM Symposium on
Principles of Programming Languages, 1989.
 Advisory Board for Foundations of Computation Laboratory, Key
Centre for Software Technology, Department of Computer Science, The
University of Queensland, 1989present.
 National Science Foundation SmallScale Institutional
Infrastructure Panel, June 1990.
 Founded the Association of Electronic Scholarly Journals, 1990.
 New York Statewide Review of Doctoral Programs, site visitor,
October 1990.
 Universities Space Research Association Science Councils: CESDIS
19911996, ICASE 19911992.
 Conference cochair for research contributions
Constructivity in Computer Science, 1991.
 NSF/CRA Workshop on the Computing Research Infrastructure, July
1991.
 Advisory Board for the Information Science Research Institute at
the University of Nevada, Las Vegas, 19911994.
 Organizing Committee, Third International Conference on
Algebraic Methodology and Software Technology, 19921993.
 Organized Annual NSF Infrastructure Workshop, June 1993.
 Chair of ACM SIGSOUND, 20012003.
University Administration and Service
Purdue University
 Dept. of Computer Sciences Undergraduate Committee, 19771978.
 Organized Theoretical Computer Science Seminar, 19781983.
 School of Science Student Cases Committee, 19781980.
 Science Board (renamed Science Council), a faculty/student
service organization in the School of Science, 19781983.
 Dept. of Computer Sciences Faculty Secretary, 19791981.
 Faculty advisor to Purdue Velo Club, 19801981.
 Faculty advisor to Purdue Ethnic Dancers, 19801983.
 Graduate Council, 19801983.
 School of Science Grade Appeals Committee, 19801983.
 Department of Computer Sciences Personnel Committee, 19811983.
 Evaluated Purdue Fellowship Candidates, 1980.
 Evaluated Purdue Summer XL Proposals, 1982.
 PALS program computer demonstration for high school students,
19791982.
 Lecture to high school students on careers in Computer Science,
1981.
 Special Graduate School committee to study retention of female
graduate students, 19821983. Produced a detailed multifactor
statistical study of graduate student retention at Purdue.
 Department of Computer Sciences Head Search Committee, 1983.
The Johns Hopkins University
 CSNet Liaison, 19831985.
 Engineering Computing Facility Advisory Committee, 19831985.
 Chairman, Faculty Search Committee, 1984.
 Ad Hoc Committee to Study Fiber Optic Network, 1984.
 Facilities Manager for EECS UNIX 19841985. Installed two VAX
11/750 systems running UNIX 4.2 BSD.
The University of Chicago
 Graduate Committee, 19851987.
 McCormick Fellowship Selection Committee, 1986.
 Associate Chairman, Department of Computer Science, 19861987.
 Chairman, Department of Computer Science, 19871990.
 Board of Computing Activities and Services, 19861990; Steering
Committee 19891994.
 Ethernet Management Committee, 1986.
 Review Committee for the Mathematics and Computer Science
Division at Argonne National Laboratory, 19871992. Chairman,
19901992.
 Chairman of Working Group on Data Communications, 19871988.
 Working Group on Public Computing, 19871988.
 Supervised design and renovation of Ryerson 4th floor to add
4,000 square feet of graduate student offices, lounge, etc.,
19871991.
 Working Group on HighPerformance Computing, 19881989.
 Designed university statute and policy on intellectual property
rights to software developed on campus, 1989.
 Chairman of Public Computing Policy Committee, 19901991.
 Committee on Patents, Software, and Intellectual Property,
19891993, chairman 19921993.
 Communications Architecture Committee, 19911995.
 Library Board, 19911994.
 Chairman of C.S. Dept. Computing Facilities Committee,
19911999, 2000present.
 Council on Research, 19921993.
 Provost's Faculty Task Force on Library Migration (studying
changes to library computer systems) 19931994.
 Council of the University Senate, 19941996.
 Faculty advisor to University of Chicago Student Computing
Operation, 1994present; Student Linux Users Group 1997present.
 Board of Computing Activities and Services, standing committee
on networking, 19951997.
 Faculty Advisory Committee for The Challenge of Modern
Democracy, an interdisciplinary conference held 910
April 1998 at the University of Chicago.
 Advisory Board to create a new program in Interactive Media in
the Graham School of General Studies, 19972000.
 Planning committee for Franke Institute and Computation
Institute joint lecture series on "Design and
Information/Communication Technologies," 20002004.
 Physical Sciences Division Computing Committee, 20002004.
 Coach the University of Chicago Programming Team, 1998present.
The team competed in the World Finals in 2001, 2002, 2009, 2010, 2011.
 Physical Sciences Division Advisory Committee for the Center for
Elementary Mathematics and Science Education, 20022005.
 Computer Science Professional Programs Faculty Oversight Committee,
20022008.
 Faculty advisor for student chapter of the Association for
Computing Machinery, 1999present.
 Faculty advisor for the Secular Student Alliance,
2010present.
Community Service
 Interviewed for the radio program ``Science Alive!'' April,
1986.
 Glencoe IL School District 35 Strategic Planning Retreat
December, 1991.
Research Grants and Contracts
 A Uniform Theory for Implementations of Descriptive
Languages (with C. Hoffmann $5,400) Purdue Summer XL grant,
1978.
 A Uniform Theory for Implementations of Descriptive
Languages (with C. Hoffmann $71,117) National Science
Foundation, 19781980.
 A Uniform Theory for Implementations of Descriptive
Languages (with C. Hoffmann $160,659) National Science
Foundation, 19811983.
 Research on Programming with Equations (with C. Hoffmann
$116,149) National Science Foundation, 19831985.
 Highly Parallel Architectures for GeneralPurpose
Concurrent Programming Languages (with G. Masson $57,940)
National Security Agency, 19841985.
 Equational Logic as a Programming Language ($27,500)
Louis Block Fund, 19851986.
 Equational Logic as a Programming Language ($185,193)
National Science Foundation, 19861988.
 Theory and Implementation of Equational Logic Programming
($176,333) National Science Foundation, 19881990.
 The University of Chicago Computer Science Laboratory
($2,030,221) National Science Foundation, 19891994.
 Rigorous Mathematical Sciences Curriculum for the
Humanities and Social Sciences ($50,000) National Science
Foundation 19901992.
 Theory and Implementation of Equational Logic Programming
($161,136) National Science Foundation, 19911993.
Meetings Attended
 17th Annual Symposium on Foundations of Computer Science,
Houston, 1976.
 9th Annual Symposium on Theory of Computing, Boulder,
1977.
 19th Annual Symposium on Foundations of Computer Science,
Ann Arbor, 1978.
 6th Annual Symposium on Principles of Programming
Languages, San Antonio, 1979.
 11th Annual Symposium on Theory of Computing, Atlanta,
1979.
 Frege Conference, Friedrich Schiller Universität, Jena,
DDR, 1979.
 12th Annual Symposium on Theory of Computing, Los Angeles,
1980.
 21st Annual Symposium on Foundations of Computer Science,
Syracuse, 1980.
 Verification Workshop, Yorktown Heights, NY, 1981.
 13th Annual Symposium on Theory of Computing, Milwaukee,
1981.
 Workshop on Recursion Theoretic Aspects of Computer
Science, W. Lafayette IN, 1981.
 14th Annual Symposium on Theory of Computing, San
Francisco, 1982.
 23rd Annual Symposium on Foundations of Computer Science,
Chicago, 1982.
 15th Annual Symposium on Theory of Computing, Boston,
1983.
 24th Annual Symposium on Foundations of Computer Science,
Tucson, 1983.
 Brooklyn College Symposium on Theoretical Computer Science
I: Logic in Computer Science, 1983.
 11th Annual Symposium on Principles of Programming
Languages, Salt Lake City, 1984.
 International Symposium on Logic Programming, Atlantic
City, 1984.
 1984 Conference on Information Sciences and Systems,
Princeton NJ.
 16th Annual Symposium on Theory of Computing, Washington
DC, 1984.
 25th Annual Symposium on Foundations of Computer Science,
West Palm Beach, 1984.
 University of Maryland Special Year in Mathematical Logic
and Theoretical Computer Science, 19841985.
 12th Annual Symposium on Principles of Programming
Languages, New Orleans, 1985.
 Logics of Programs Workshop, Brooklyn New York, 1985.
 26th Annual Symposium on Foundations of Computer Science,
Portland OR, 1985.
 13th Annual Symposium on Principles of Programming
Languages, St. Petersburg FL, 1986.
 Workshop on Theoretical Aspects of Reasoning About
Knowledge, Asilomar CA, 1986.
 SIGPLAN 1986 Symposium on Practical Program Development
Environments, Palo Alto CA.
 14th Annual Symposium on Principles of Programming
Languages, Munich, 1987.
 Colloquium on Resolution of Equations in Algebraic
Structures, Lakeway, Texas, 1987.
 2nd International Conference on Rewriting Techniques and
Applications, Bordeaux, 1987.
 SIGPLAN 1987 Symposium on Interpreters and Interpretive
Techniques, St. Paul MN.
 15th Annual Symposium on Principles of Programming
Languages, San Diego CA, 1988.
 1988 Snowbird Meeting of CS and EECS Department Chairs,
Snowbird UT.
 National Computer Conference, Louisville KY, 1988.
 16th Annual Symposium on Principles of Programming
Languages, Austin TX, 1989.
 3rd International Conference on Rewriting Techniques and
Applications, Chapel Hill NC, 1989.
 17th Annual Symposium on Principles of Programming
Languaes, San Francisco CA, 1990.
 1990 CER/II Meeting, Atlanta GA, 1990.
 Association of Research Libraries Meeting about Refereed
Academic Electronic Publishing Projects, Raleigh NC, 1990.
 Symposium on Constructivity in Computer Science, San
Antonio TX, 1991.
 NSF/CRA Workshop on the Computing Research Infrastructure,
Washington DC, 1991.
 19th Annual Symposium on Principles of Programming
Languages, Albuquerque NM, 1992.
 Symposium on Character Recognition and Document Analysis,
Las Vegas NV, 1992.
 Conference on Academic and Professional Journals in the
Twentieth Century, Chicago IL, 1992.
 Association for Symbolic Logic, Annual Meeting, South Bend
IN, 1993.
 Annual NSF Infrastructure Workshop, 1993.
 8th Annual IEEE Symposium on Logic in Computer Science,
Montreal Québec, 1993.
 Seminars on Academic Computing, University Executive
Program, 1993.
 International Conference on Refereed Electronic Journals,
Winnipeg Manitoba, 1993.
 Mathematical Foundations of Computer Science 1994  19th
International Symposium, Kosice, Slovakia, 1994
 Acoustical Society of America, Indianapolis, 1996.
 Professors and Publishing in the Electronic Academy. The
University of Tennessee, Knoxville Library, 1996.
 Acoustical Society of America, Seattle, 1998.
 COST Digital Audio Effects Workshop (DAFx99)), Trondheim,
Norway, 1999.
 Acoustical Society of America, Chicago, 2001.
 National Science Foundation Summit on Future Internet
Architecture, Arlington VA, October 1215 2009 (by invitation).
Unrefereed Lectures
 Rigorous Development of a Lucid Interpreter. University of
Waterloo, Fall 1976.
 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.
 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.
 Logic For Reasoning About Programs. Purdue University, April
1977; Humboldt Universität, E. Berlin, 15 May, 1979.
 A Critique of the Foundations of HoareStyle 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.
 The Intuitive Foundations of Programming Logic. New Mexico
Tech., 22 September, 1980; Los Alamos Laboratories, 24 September,
1980.
 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.
 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;
CarnegieMellon 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 SophiaAntipolis, France, 22 May, 1987.
 Lower Bounds for Sorting With Realistic Instruction Sets.
University of Chicago, 7 February, 1985.
 FaultTolerant Logic for Automated Reasoning. SUNY Stony Brook,
20 February, 1985; University of Amsterdam, 16 January, 1987.
 Semantics for Infinite and Indeterminate Computations in Logic
Programming Languages. Midwest Theory of Computation Meeting,
Purdue, 19 April, 1986.
 Intuitive Constructive Semantics for Constructive Logic. Midwest Theory of Computation Meeting, University of Illinois, 15
April, 1987.
 A Compiler for Equational Logic Programs. Midwest Society
for Programming Languages and Systems, University of Illinois,
Spring, 1988.
 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.
 Meaningful Semantics for Constructive Logic. University of
Maryland, 2 May, 1990; Universität Würzburg, 10 November, 1990.
 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.
 Applications of Logic to Programming Language Design and
Implementation. The Johns Hopkins University, 17 December, 1992.
 Term ToursI/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.
 Electronic Publication, Refereeing, and the Economy of
Attention. University of Chicago, Physics Department, 7 October,
1993.
 Intuitive Counterexamples for Constructive Fallacies. SUNY
Buffalo, 7 October 1994.
 Electronic Journals  scholarly invariants in a changing
medium. SUNY Buffalo, 7 October 1994; Dartmouth, 26 October 1994.
 Digital Sound Synthesis. Wesleyan University, 25 October 1994;
Dartmouth, 26 October 1994; Carleton College, 30 January 1996.
 Program Execution as Logical Deduction. Macalester College, 31
January 1996.
 Leveled Garbage Collection. The University of Iowa, 13 April 1998.
 Minimal publickey infrastructure. USTC Hefei, 2000.
 Why is PNP so Hard to Prove? Chinese Academy of Science,
Beijing, 11 September 2003.
 Prediction vs. Commitment in Garbage Collection. USTC Hefei,
September 18 2003.
 Minimal publickey infrastructure. Wesleyan University, November 15 2004.
 The relevance of relevance. Universidad Complutense de Madrid, June 12 2006.
 Endtoend publickey infrastructure. Universidad Politecnicá de Madrid, July 5 2006.
 Timefrequency analysis. Reed College Math Colloquium, September 9 2010.
 The sources of certainty in computation and formal systems, University of Chicago Formal Philosophy Workshop, November 23 2010.
Consulting and Visiting
 Prof. R. Constable, Cornell University, type theory, 1331
July 1981.
 Prof. D. Stanat, University of North Carolina, equational logic
programming, 1920 March 1984.
 Drs. N. Gehani and P. Wolper, AT&T Bell Laboratories,
concurrent C, programming logic, December 1984 to April
1985.
 Drs. J. Williams, E. Wimmers and J. Backus, IBM Almaden
Research Center, functional programming languages, 2325 October 1990.
 Professeur Associé at Université de Bordeaux 1, Unité
Formation et Recherche de Mathématique et d'Informatique, 16 March
to 17 April 1993.
 Chicago Department of Aviation, Y2K date problem, December 1998
through December 1999.
 Internal Revenue Service, expert
testimony on research tax credit, February 1999 through May 2000.
 Illinois Attorney General, FDC failures, 20002003.
 Universidad Politecnicá de Madrid, Spring 2006.
M.S. Students
 The University of Chicago
 Susanne Lefvert (visiting from Lulea University of Technology), 20012002, user interface for Loris
sound synthesis/morphing/analysis.
Ph.D. Students
 Purdue University
 Paul Chew, 19791981, Normal Forms in Term Rewriting
Systems.
 Eric Dittert, 19801982, On the Complexity of Retrieving
Information.
 The Johns Hopkins University
 Robert Strandh, 19831987, Compiling Equational Programs
into Efficient Machine Code.
 The University of Chicago
 Samuel Rebelsky, 19871993, Tours, a System for Lazy
TermBased Communication.
 David Sherman, 19871994, RunTime and CompileTime
Improvements to Equational Programs.
 Donald Ziff, 19891995, Lazy Functional Programming for
FullText Information Retrieval.
 Stephen Bailey, 19881995, Hielp, a Fast Interactive Lazy
Functional Language System.
 Guanshan Tong, 19931997, Design and Evaluation of a
HighPerformance Automatic Memory Management System.
 Ilya Bisnovatyi, 19932006 (withdrew), sound synthesis.
Postdoctoral Associates
 William Winsborough, 198890.
 Yiyun Chen, 198991.
Courses Taught
 Numerical Analysis
 Introductory Programming in Pascal, Fortran, Scheme
 Data Structures
 Theory of Computation
 Algorithm Design and Analysis
 Programming Languages
 Digital Sound Modeling
 Operating Systems
 Advanced Operating Systems
 Computation, Information and Description (concerning
applications of computational ideas to philosophy, mathematics,
physics, biology, etc.)
 Computer Architecture
 Free Software Practicum
 Program Verification
 Constructive Logic
 Digital Sound
 Theory of Computation
 Algorithm Design and Analysis
 File Structures
 Computational Complexity
 Logic Programming
 Lambda Calculus
 Operating Systems
 Advanced Operating Systems
 Computer System Administration
 Computer Architecture
 Mathematical Transforms for Signal Processing
 Big Ideas in Computer Science
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) 
WinterSpring 
1986 
ComSci 388 Logic Programming Languages III (G) 
WinterSpring 
1987 
ComSci 488 The Lambda Calculus (G) 
WinterSpring 
1988 
ComSci 388 Logic Programming Languages III (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) 
This document was generated using the
LaTeX2HTML translator Version 200221 (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 20110127
Mike O'Donnell
20110127