Curriculum Vitae

October 17, 1996

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

Math Dept. fax: (860) 685-2571

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

Education University of Nebraska-Lincoln, 1977. B.Sc. in Mathematics. Minors: Physics, English Cornell University, 1979. M.Sc. in Mathematics Cornell University, 1990. M.Sc.in Computer Science. Ph.D. in Mathematics. Dissertation:

Relating Kripke Models and Realizability. Advisor: Prof. Anil Nerode.

Teaching and Research Appointments Current: Asst. Prof. of Computer Science, Dept. of Mathematics, Wesleyan University, 1993-Instructor, Dept. of Mathematics, University of Pennsylvania, 1990-1993. Visiting Scientist, Mathematical Sciences Institute (MSI), Cornell, summer 1991. Postdoctoral Research Associate, Dept. of Computer Science and MSI, Cornell University,

Jan.-Sept., 1990.

Visiting appointments Visiting Researcher, Isaac Newton Institute, Cambridge University, August-September 1995. Visiting Professor of Computer Science, University of Nancy, France, May-June 1994 & 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, Logic Programming and Expert Systems, Mathematical Sciences Institute, Cor-

nell, 1987-90.

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

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

Research Interests

Relational Programming, Categories and Logic Programming, Intuitionistic Semantics, Constructive Set Theory, Linear Logic.

Publications

Refereed Publications:

[1] “Some Intuitions Behind Realizability Semantics for Constructive Logic: Tableaux and Läuchli Countermodels” Annals of Pure and Applied Logic, pp. 187-239, vol 81, Elsevier North-Holland, (with Michael O’Donnell), 1996.

[2] “Type Theory and Inhabitation: A Constructive Completeness Theorem for Martin-Löf Type Theory” to appear in the Annals of Pure and Applied Logic , 31 pp., 1996.

[3] “Combinatory Logic Programming: Computing in Relation Calculi” in Proceedings of the 1994 International Symposium on Logic Programming, M. Bruynooghe, ed., M.I.T. Press, pp. 269-285, (with Paul Broome), 1994.

[4] “Logic Programming in Tau-Categories”, in Computer Science Logic ’94 , LNCS 933, Springer, pp. 249-263, (with Peter Freyd and Stacy Finkelstein), 1995.

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

[6] “Constructive Kripke Semantics and Realizability”, in Logic from Computer Science, Y. N. Moschovakis, ed., MSRI Publications, vol. 21, Springer, pp. 319-358, 1992.

[7] “Kripke Semantics for Dependent Type Theory and Realizability Interpretations”, in Constructivity in Computer Science, LNCS 613, Springer Verlag, pp. 22-31, 1991.

Invited publications:

[8] “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, pp. 257-364, 1994.

[9] “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, pp. 87–111, (with Michael O’Donnell), 1994.

Journal Submissions:

[10] “A New Framework for Declarative Programming” submitted to Theoretical Computer Science, 48 pp., (with Peter Freyd and Stacy Finkelstein), 1996.

Technical Reports:

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

“Realizability and Kripke Forcing”, Technical Report 90-1163, Dept. of Computer Science, Cornell University, 1990. Included in “Type Theory and Inhabitation”, cited above.

“Some Kripke Models for ‘One-Universe’ Martin Löf Type Theory”, Technical Report 90-1162, Dept. of Computer Science, Cornell University, 1990. Extended version appeared as “Kripke Semantics for Dependent Type Theory and Realizability Interpretations”, cited above.

In preparation:

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

“Logic Programming and Propositions-as-Types: A Realizability Interpretation of declarative Programs”(a preliminary abstract appeared in the electronic proceedings of the Types Basic Research Action Workshop, Baastad, Sweden.)

“Cartesian Logic and Constraints”, with Peter Freyd.

Short Courses Taught:

2-week 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)

2-week course on Linear Logic, Uniform Proof Systems, Categories and Logic Programming, Bahía Blanca, Argentina. August 1996.

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”, 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”, paper, 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, 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.

“Logic Programming and Propositions-as-Types: A Realizability Interpretation of declarative Programs”, invited address, TYPES Basic Research Action (Esprit) workshop, Baastad, Sweden, June 1992.

“The Complexity of some Fragments of Linear Logic”, talk, 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, July 1995.

“Categorical Logic programming”, invited talk, University of Pisa, July 1995.

“Relational Programming”, invited talk, Oxford University, Sept. 1995.

“Categories and Logic programming”, presented at the workshop by the same name, Isaac Newton Institute, Cambridge University, Sept. 1995.

“A Categorical Framework for Logic Programming”, invited presentation, Extensions of Logic Programming ’96, Leipzig, March 1996.

“Categories, Allegories, and Logic Programming”, invited talk, 60th birthday celebration in honor of Peter Freyd, University of Pennsylvania, April 1996.

Workshops:

Organized “Categories and Logic programming” workshop, Isaac Newton Institute, Cambridge University, Sept. 1995.

Grants:

• 1992-1995: Programming with Relations, ONR, $ 300,000, Co-PI with Peter Freyd, Penn.

• 1995-1997: Categorical and Relational Logic Programming, ONR, $ 200,000, co-PI’s Peter Freyd, Penn, Dan Dougherty, Wesleyan, Stacy Finkelstein, McGill.

• 1995-1996: Travel grant to participate in the Semantics of Computation programme, Newton Institute, Cambridge University, Fall ’95, ONR, $20,000, co-PI: Peter Freyd, Penn.

Current Ph. D. Students:

• Robert McGrail, Wesleyan University, topic: Monads, Control and Side Effects in Logic Programming.

• Mary de Marco, Wesleyan University, topic: Categorical Proof Theory and Semantics of Linear Logic Constraint Programming Languages.

• Claudio Gutierrez, Wesleyan University, topic: Relational and Functional Programming.

Current M. A. Students:

• Matt Ruhlen, Wesleyan University, Relational Compilation of Declarative Programs.