Papers

this directory contains

1."cahiers.*"  the paper "Realizability, Set Theory and Term Extraction"
from "The Curry-Howard Isomorphism" (volume 8 of the 
Cahiers du Centre Logique de L'Universite Catholique de Louvain), 1995.

2. "tbll93.*" "The Decidability of TBLL",
 written jointly with Jawahar Chirimar, Penn.
 a decision method for the Tensor-Bang fragment of Linear Logic,
with NP lower bound and double-exponential upper bound. Published 
in CSL'91 proceedings and (in expanded version) as a U.Penn 
CIS Tech report in 1993.

3."dist-mscs94.dvi" "Intuitive Counterexamples for Constructive Fallacies"
written jointly with Michael O'Donnell, Univ. of Chicago, 
appeared in proc. MSCS-94, Slovakia, in LNCS 841, springer.
   A Relational Realizability Model for Intuitionistic Logic, extending
Lauchli's abstract realizability.

4.dist-ilps94.*:  Combinatory Logic Programming: Programming with Relations.
written with Paul Broome. Expanded version of the paper that appeared in 
   Proc. Int. Logic Programming Symp. '94, MIT Press
                       [see 1997 paper: item 8 in this list] 

5.tauLP-dist.*:  Logic Programming in Tau Categories.
written with Peter Freyd and Stacy Finkelstein.
Revised version of a paper that appeared in Proc. Computer Science
Logic '94, LNCS 933, Springer. 

6.   circKleene96.ps "Some Intuitions Behind Realizability
Semantics for Intuitionistic Logic: Tableaux and Lauchli
Countermodels", written jointly with Michael O'Donnell, Univ. of
Chicago,  appeared in the Annals of Pure and Applied Logic 81, 1996.

    A Tutorial-style treatment of Lauchli semantics. 

   [We give a detailed generalization of L\"auchli's proof of
    completeness for the propositional part of the Heyting Calculus,
    stressing arbitrary abelian groups rather than cyclic ones.

    In our treatment, we establish some new results about L\"auchli
    models. We show how to extend the sconing and gluing constructions
    familiar from Kripke and Frame semantics and Topos theory, to
    L\"auchli models, and use them to give an algebraic approach to
    countermodel construction.]


7.  syntaxroot.* : "A New Framework for Declarative
Programming", Freyd-Finkelstein-Lipton: Categorical Semantics for 
Weak Hereditarily Harrop logic programs with constraints. to appear in TCS.  


8. relmics.* (1997: Last revised JUNE 28): 

   "Some Notes On Logic Programming with a Relational Machine", by Jim
Lipton and Emily Chapman. A compilation of Horn Clause programs into
executable variable-free terms in an equational relation calculus.

Substantially modifies and improves translation in dist-ilps94.*, and
supplies proofs of correctness and completeness of evaluation.

9. alpdist98.* (1998)
Updated manuscript of ALP 98 paper 

 "Encapsulating data in  Logic Programming via Categorical Constraints"

with Robert McGrail. Extends Horn Clause foundation defined in 7. to
include a data type specification formalism.

10. uniform.* (1999, revised Jan 2002) with Mary de Marco: Uniform Algebras: a
complete Declarative and Operational Semantics for the HOHH logic
of lambda-Prolog.

11. lpar01.ps (2001) with Gianluca Amato:

  "Indexed Categories and Bottom-Up Semantics of Logic Programs"