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"

Last modified: Thu May 9 19:13:13 EDT 2002