% BIB FILE FOR PAPERS SUPPORTED BY EPSRC L54639 % entries for Levy @InProceedings{Levy99, author = {P.B Levy}, title = {Call by push-value: a subsuming paradigm}, booktitle = {Typed $\lambda$-calculus and Applications}, year = 1999, editor = {J-Y. Girard}, volume = 1581, series = {Lecture Notes in Computer Science}, publisher = {Springer} } % entries for O'Hearn @article{OP99, author = "P.W. O'Hearn and D.J. Pym", journal= "Bulletin of Symbolic Logic", volume=5, number=2, pages ="215-244", title = "The Logic of Bunched Implications", year="June 1999" } @Article{OHearn98, author = {P.W. O'Hearn}, title = {Polymorphism, Objects and Abstract Types}, journal = {SIGACT News}, year = 1998, volume = 29, number = 4, pages = {39-40}, month = {December} } @unpublished{OHearn00, author = "P.W. O'Hearn", title = "On Bunched Typing", note = "Submitted to Journal of Functional Programming", year = 2000 } @unpublished{OPY00, author = "P. O'Hearn and D. Pym and H. Yang", title = "Possible worlds and resources: the semantics of {BI}", note = "Submitted to Theoretical Computer Science" } @InProceedings{OHearn99, author = {P.W. O'Hearn}, title = {Resource Interpretations, Bunched Implications and the $\alpha\lambda$-calculus}, booktitle = {Typed $\lambda$-calculus and Applications}, year = 1999, editor = {J-Y. Girard}, volume = 1581, series = {Lecture Notes in Computer Science}, publisher = {Springer} } % entries for Pym @unpublished{Pym00SearchNotes, author = "D. Pym", note= "Manuscript: available at http://www.dcs.qmw.ac.uk/~pym", title = "Notes towards a semantics for proof-search", year ="2000" } @article{RPW2000a, author="E. Ritter D.J. Pym and L.A. Wallen", title="On the intuitionistic force of classical search", journal="Theoretical Computer Science", volume="232", pages="299-333", year="2000" } @article{RPW2000b, author="E. Ritter D.J. Pym and L.A. Wallen", title="Proof-terms for classical and intuitionistic resolution", journal="J. Logic Computat.", volume="10(2)", pages="173-207", year="2000" } @unpublished{PR00a, author="D. Pym and E. Ritter", title="On the semantics of classical disjunction", note="To appear: \emph{Journal of Pure and Applied Algebra}", } @article{IshtiaqPym98, author = "S.S. Ishtiaq and D.J. Pym", journal= "Journal of Logic and Computation", title = "A Relevant Analysis of Natural Deduction", volume="8(6)", pages="809-838", year="1998" } @inproceedings{IshtiaqPym99, author = "S.S. Ishtiaq and D.J. Pym", title = "Kripke resource models of a dependently-typed, bunched $\lambda$-calculus (extended abstract)", booktitle="Computer Science Logic", series="LNCS", editor="J. Flum and M. Rodr\'{\i}guez-Artalejo", volume="1683", publisher="Springer", pages="235-249", year="1999" } @techreport{IshtiaqPym00, author="S. Ishtiaq and D. Pym", title="Corrections and Remarks", number="RR-00-04. ISSN 1470-5559.", year="2000", institution="Department of Computer Science, Queen Mary and Westfield College, University of London", address="London", type="Research Report" } @unpublished{IshtiaqPym98a, author = "S.S. Ishtiaq and D.J. Pym", note= "Submitted: manuscript available at http://www.dcs.qmw.ac.uk/$\sim$pym", title = "Kripke resource models of a dependently-typed, bunched $\lambda$-calculus" } @book{Pym00Mono, author="D.J Pym", title="The semantics and proof theory of the logic of bunched implications", year="2000", note="forthcoming monograph" } @article{GalmichePym00, author="D. Galmiche and D. Pym", title="Proof-search in type-theoretic languages: an introduction", journal="Theoretical Computer Science", volume="232", pages="5-53", year="2000" } @article{OP99, author = "P.W. O'Hearn and D.J. Pym", journal= "Bulletin of Symbolic Logic", volume=5, number=2, pages ="215-244", title = "The Logic of Bunched Implications", year="June 1999" } @inproceedings{Pym99LICS, author = "D.J. Pym", booktitle= "Proc. LICS'99", publisher = "IEEE Computer Society Press, 1999", year = "1999", title = "On Bunched Predicate Logic", pages = "183-192" } @unpublished{Pym98a, author = "D.J. Pym", note= "1998. Available on the web at http://www.dcs.qmw.ac.uk/$\tilde{\quad}$pym, superceded by \cite{Pym00Mono}", title = "The Semantics and Proof Theory of the Logic of Bunched Implications, {I}: Propositional {\BI}" } @unpublished{Pym98b, author = "D.J. Pym", note= "1998. Superceded by \cite{Pym00Mono}", title = "The Semantics and Proof Theory of the Logic of Bunched Implications, {II}: Predicate {\BI}" } @article{Pym98c, author = "D.J. Pym", journal="Electronic Notes in Theoretical Computer Science", month="", year=1998, volume="17", number="", title = "Logic Programming with Bunched Implications (Extended Abstract)", note="24 pages" } % entries for Robinson @unpublished{DeMarchiRobinsonRosolini:mfps2000, author = {F. De Marchi and E.P. Robinson and G. Rosolini}, title = {An Abstract Look at Realizability}, note = {in preparation} } @InProceedings{PowerRobinson:ppdp2000, author = {A.J. Power and E.P. Robinson}, title = {Logical Relations, Data Abstraction and Structured Fibrations}, booktitle = {Proceedings of the Second International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00)}, OPTcrossref = {}, OPTkey = {}, pages = {15-23}, year = {2000}, editor = {Maurizio Gabrielli and Frank Pfenning}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, publisher = {ACM Press}, OPTnote = {Proceedings of the Second International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00)}, OPTannote = {} } @InProceedings{PowerRobinson:csl2000, author = {A.J. Power and E.P. Robinson}, title = {Logical Relations and Data Abstraction}, booktitle = {Proceedings of Computer Science Logic 2000}, OPTcrossref = {}, OPTkey = {}, OPTpages = {497-511}, year = {2000}, editor = {Peter Clote and Helmut Schwichtenberg}, OPTvolume = {1862}, OPTnumber = {}, series = {Lecture Notes in Computer Science}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, publisher = {Springer Verlag}, note = {}, OPTannote = {} } @Article{PowerRobinson:mfps99, author = {John Power and Edmund Robinson}, title = {Modularity and Dyads}, journal = {Electronic Notes in Theoretical Computer Science}, year = 1999, volume = 20, pages = {14pp}, note = {http://www.elsevier.nl/} } @Article{PowerRobinson:mscs97, author = {John Power and Edmund Robinson}, title = {Premonoidal categories and notions of computation}, journal = {Mathematical Structures in Computer Science}, year = 1997, volume = 7, pages = {453-468} } % BibTeX file for Hayo Thielecke % % Last update 12.08.2000 @unpublished{HayoDB, author = "Hayo Thielecke", title = "Comparing control constructs by typing double-barrelled {CPS} transforms", note = "Submitted to the 2001 Continuations Workshop" } @inproceedings{Thieleckeexncontstate, author = {Hayo Thielecke}, title = {On Exceptions versus Continuations in the Presence of State}, booktitle = {Programming Languages and Systems, 9th European Symposium on Programming, {ESOP} 2000,}, year = 2000, editor = {Gert Smolka}, publisher = {Springer Verlag}, series = {LNCS}, number = 1782, pages = {397--411}, } @article{Thieleckecontfunjump, author = {Hayo Thielecke}, title = {Continuations, functions and jumps}, journal = {SIGACT News}, publisher = {{ACM} Press}, year = 1999, month = Jun, volume = 30, number = 2, pages = {33--42}, } @inproceedings{PowerThielecke99, author = {John Power and Hayo Thielecke}, editor = {{J\v\i r\'\i} Wiedermann and Peter {van Emde Boas} and Mogens Nielsen}, title = {Closed {F}reyd- and kappa-categories}, booktitle = {Proceedings {ICALP '99}}, pages = {625--634}, year = 1999, publisher = {Springer Verlag}, series = {LNCS}, number = 1644, } @inproceedings{RieckeThielecke99, author = {Jon G. Riecke and Hayo Thielecke}, title = {Typed Exceptions and Continuations Cannot Macro-Express Each Other}, editor = {{J\v\i r\'\i} Wiedermann and Peter {van Emde Boas} and Mogens Nielsen}, booktitle = {Procedings {ICALP '99}}, pages = {635--644}, year = 1999, publisher = {Springer Verlag}, series = {LNCS}, volume = 1644, } @article{Thieleckeusingtwice, author = {Hayo Thielecke}, title = {Using a continuation twice and its implications for the expressive power of {\tt call/cc}}, journal = {Higher-Order and Symbolic Computation}, editor = {Robert R. Kessler and Carolyn Talcott}, pages = {47--74}, year = 1999, volume = 12, number = 1, publisher = {Kluwer}, } @article{Thieleckehtlandinintro, author = {Hayo Thielecke}, title = {An introduction to {L}andin's ``{A} Generalization of Jumps and Labels''}, journal = {Higher-Order and Symbolic Computation}, editor = {Robert R. Kessler and Carolyn Talcott}, year = 1998, volume = 11, number = 2, pages = {117--124}, publisher = {Kluwer}, }