Curriculum Vitae

May 20, 1996

James Lipton Dept. of Mathematics Wesleyan University Middletown CT 06459-0128 Telephone: (203) 685-2188 (home:) (203) 344-8246

                                       e-mail: lipton@allegory.cs.wesleyan.edu

Education

University of Nebraska-Lincoln,1972-1977. B.Sc. in Mathematics, Minors in Physics and English

Cornell University, 1977-1979. M.Sc. in Mathematics

Cornell University, 1983-1989. Ph.D. in Mathematics, M.Sc. in Computer Science

Teaching and Research Appointments

Current Employment: Asst. Professor of Computer Science, Dept. of Mathematics, Wesleyan University, 1993-

Instructor, Dept. of Mathematics, University of Pennsylvania, Jun 1990-Jan 1993.

Visiting Scientist, Mathematical Sciences Institute, Cornell, summer 1991.

Postdoctoral Research Associate, Dept. of Computer Science and Mathematical Sciences Institute, Cornell University, Jan. 1990-Sept.1, 1991

Visiting appointments

Visiting professor of computer science, University of Nancy, France, May-June 1994. May-June 1995.

Fellowships

Sloane Dissertation Fellow, July, 1988 – August, 1989

MSI Graduate Research Fellow, 1987-88, summer 1987, summer 1988

Hutchinson Fellow, spring 1987

Work Experience

Consultant on Logic Programming and Expert Systems, Mathematical Sciences Institute, Cornell, 1987-90.

Languages Fluent in written and spoken Spanish, comfortable with spoken French.

\underline{J. Lipton: C.V.} 2

Publications^{1}

Relating Kripke Models and Realizability, Ph.D. Dissertation, Cornell, 1990, advisor: Prof. Anil Nerode.

∗ “Constructive Kripke Models and Realizability”, in Logic for Computer Science, MSRI Publications, Springer 1992.

“Logic Programming in Constructive Type Theory”, 1990. Internal Technical Report, Dept. of Computer Science, Cornell University, revised 1991.

“Realizability and Kripke Forcing”, Technical Report 90-1163, Dept. of Computer Science, Cornell University, 1990.

“Some Kripke Models for ‘One-Universe’ Martin Löf Type Theory”, Technical Report 90-1162, Dept. of Computer Science, Cornell University, 1990.

“Kripke Semantics for Dependent Type Theory and Realizability Interpretations”, in Constructivity in Computer Science (proceedings from the 1991 conference, San Antonio), LNCS 613, Springer Verlag.

“Type Thory and Inhabitation: A Constructive Completeness Theorem for Martin-Löf Type Theory” submitted to the Annals of Pure and Applied Logic .

“Realizability, Set Theory and Term Extraction”, in The Curry-Howard Isomorphism: 8-ème volume des cahiers du centre de logique de l’Universite Catholique de Louvain, 1994.

∗ with J. Chirimar: “Provability in TBLL (the Tensor Bang Fragment of Linear Logic)”, in Computer Science Logic (proceedings of CSL ’91, Bern), LNCS 613, Springer-Verlag. Expanded version appeared as Univ. of Pennsylvania Technical report, 1993

with Paul Broome: “Combinatory Logic programming: Computing in Relation Calculi” in Proceedings of the 1994 International Symposium on Logic Programming, M. Bruynooghe, ed., M.I.T. Press.

with Michael O’Donnell: “Intuitive Counterexamples for Constructive Fallacies”, in Mathematical Foundations of Computer Science 1994 — 19th International Symposium, MFCS ’94, Kosice, Slovakia, August 1994 — Proceedings, Lecture Notes in Computer Science, volume 841, Ibor Priívara, Branislav Rovan and Peter Ruz̆ic̆ka editors, Springer-Verlag, 1984, pp. 87–111.

∗ with Michael O’Donnell: “Some Intuitions Behind Realizability Semantics for Intuitionistic Logic: Tableaux and Lauchli Countermodels” to appear in the Annals of Pure and Applied Logic.

∗ with Peter Freyd and Stacy Finkelstein: “Logic Programming in Tau-Categories”, Proc. Computer Science Logic ’94, LNCS 933, Springer.

with Paul Broome: “Combinatory Relational Logic Programming”, submitted to the Journal of Logic programming.

In Preparation with Peter Freyd and Stacy Finkelstein: “A Categorical Foundation for Uniform and Constraint Logic Programming”, to be submitted to TCS. “Computing with Distributive Allegories: A Relation-based approach to Logic programming.”(Lipton-Freyd). “Logic Programming and Propositions-as-Types: A Realizability Interpretation of declarative Programs”(a preliminary version appeared in the electronic proceedings of the Types Basic Research Action Workshop, Baastad, Sweden.)

1asterisks denote refereed publications

Invited Lectures, Presentations

“Constructive Set Theory and Recursive Realizability”, invited lectures, Dept. of Mathematics, University of Turin, Italy, March 1987. “Intuitionistic ZF and Algorithm Extraction”, invited lecture, Dept. of Computer Science, Turin, Italy, March, 1987. “Intuitionistic Reasoning and Computer Science”, invited lecture, Dept. of Computer Science, Polytechnic University of Madrid, Spain, April, 1987. “Semantics for Constructive Set Theory”, invited lecture, Dept. of Computer Science, Turin, Italy, June, 1988. “Extracting Algorithms from Specifications in Constructive Set Theory”, invited lecture, University of Padua, Italy, June, 1988. “A Kripke Model for syntactic Kleene Realizability”, talk, Mid-Atlantic Math Logic Seminar, Philadelphia, winter 1988. “Abstract Realizabilities equivalent to Kripke Models”, logic seminar talk, University of Chicago, March 1990. “Relating Kripke Models and Realizability”, logic seminar talk, Dept. of Computer Science, Carnegie-Mellon University, March 1990. “Kripke Semantics for Dependent Type Theory and Realizability Interpretations”, Symposium on Constructivity in Computer Science, San Antonio, TX, June, 1991. “Logic programming, Type Theory and Fixpoints”, talk given at the Polytechnic University, Madrid, Spain, August, 1991. “The tensor-bang fragment of Linear Logic is Decidable”, paper given at the Computer Science Logic conference, October 11, 1991, Bern, Switzerland. “Kripke Semantics, Realizability and Program Synthesis”, Logic Seminar, Cornell University, Nov. 1991. “Logic Programming and Propositions-as-Types: A Realizability Interpretation of declarative Programs”, Computer Science Dept., Syracuse University, Dec. 1991. also given in a 1-hour invited talk at the TYPES Basic Research Action (Esprit) workshop, Baastad, Sweden, June 1992. “The complexity of some fragments of linear logic”: The University of Chicago, 1993 “Abstract Relational Programming”, MFPS X (workshop in the mathematical foundations of programming language semantics, Manhattan Kansas), Mar. 1994 “The Relational Full Type Hierarchy and Lauchli Models”, invited talk at Ludwig-Maximilian Univ., Munich, June 1994. “Relations in Programming languages: syntax and semantics”, invited talk, Universidad Jaume I, Castellón, Spain.

Short Courses:

• 2-week short course on lambda calculus, type theory and linear logic given at the Latin American Symposium on Mathematical Logic, ASL meeting, Bahía Blanca, Argentina. August 1992.(in Spanish).

• 5-week course in Intuitionistic and Categorical Logic, University of Nancy, France, May-June 1994. (in French)