List of papers produced by CLICS-II in year 2

This document lists all papers written by CLICS-II members, which were cited in Site Management or Topic Progress Reports. However, the reports may cite a paper with a different citation key from that given here (since the bibliographies for each report were produced independently).

Instructions for FTP

If a paper is available via anonymous FTP, then its location is given immediately below its bibliographic entry (in the format machine:/directory/filename).

For you convenience, most of these files have been collected at Imperial (without changing their filename) on the machine “theory.doc.ic.ac.uk” under the directory “CLiCS/PPR2/papers”, they are in postscript format compressed using “gzip” (use “gunzip” to uncompress them). Other papers may be available from personal directories in “theory.doc.ic.ac.uk:/papers”.

Deliverables cited by Topic Reports

The papers marked with * are available via FTP:

Topic A and G: *[CE94], *[Bra94], [HB94], *[Laf94], *[Rit94b], *[NdPR94], *[DGR94], *[PW94], *[EW94], *[JNW94], *[Win94].

Topic B: *[Hut94d], *[HJK94b], *[Haa94], [KP94], *[OR94]; *[Hut94e], *[Hut94a], *[Hut94f], *[AJ94], *[FH94]; *[Hut94c], *[Sün94b], *[PW94], *[Win94]; *[Ros94]; *[Sün94a].

Topic C: *[Acz94a], *[Dyb94d], *[Dyb94c], [Her93],*[Pit93], *[Pit94b].

Topic D: [ACC93], *[RR94], [HJ94],*[HRa], *[HRb].

Topic E and F: *[Mog94a], *[Mog94b], *[Rob94a], [Rob94b], *[Pit93], *[Pit94c], *[Sta], *[CG].

Topic H: [Coq93], [BBC94], *[Coq94a].

Topic I: *[Laf93], *[Laf94a].

Hard-copies of these papers will be available at the review meeting.

Papers cited in Site and Topic Reports

[ACC93] M. Abadi, L. Cardelli, and P.-L. Curien. Formal parametric polymorphism. Theo. Comp. Sci., 121:9–58, 1993.

[AJ94] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3. Clarendon Press, 1994. AVAILABLE from theory.doc.ic.ac.uk:/papers/Jung/handbook.dvi

[AJM94] Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF (extended abstract). In Masami Hagiya and John C. Mitchel, editors, Theoretical Aspects of Computer Software. International Symposium TACS’94, number 789 in Lecture Notes in Computer Science, pages 1–15, Sendai, Japan, April 1994. Springer-Verlag.

[Acz94a] Peter Aczel. Final universes of processes. In Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, LNCS Vol 802, pages 1–28, 1994. Edited by S. Brookes, M. Main, A. Melton, M. Mislove, D. Schmidt. AVAILABLE from ftp.cs.man.ac.uk:/pub/applied logic/PeterAczel/fup.ps

[Aczar] Peter Aczel. Schematic consequence. In D.M. Gabbay, editor, What is a logical system? Oxford University Press, To appear.

[Alt94] Thorsten Altenkirch. Consistency in ALF. In La Wintermöte ’94, Lundsbrunn, January 1994. AVAILABLE from ftp.cs.chalmers.se:/pub/clics/alti/vm.ps

[BBC94] Stefano Berardi, Marc Bezem, and Thierry Coquand. On the computational content of the axiom of choice. Technical report, technical report n 116 of the university of Utrecht, 1994.

[BGR93] Geoffrey L. Burn, Simon J. Gay, and Mark D. Ryan, editors. Theory and Formal Methods 1993: Proceedings of the First Imperial College Department of Computing Workshop on Theory and Formal Methods. Workshops in Computer Science. Springer-Verlag, 1993.

[Bra94] T. Braüner. A general adequacy result for a linear functional language. Presented at MFPS ’94. AVAILABLE from ftp.daimi.aau.dk:/pub/BRICS/RS/94/22/BRICS-RS-94-22.ps

[Bra94a] T. Braüner. A model of intuitionistic affine logic from stable domain theory. In ICALP ’94, LNCS 820, 1994. AVAILABLE from ftp.daimi.aau.dk:/pub/BRICS/RS/94/27/BRICS-RS-94-27.ps

[Bra94b] T. Braüner. The Girard translation extended with recursion. Accepted to CSL ’94, Warsaw, Poland.

[Buc94] Antonio Bucciarelli Degrees of parallelism in the continuous type hierarchy, unpublished notes, 1994. AVAILABLE from theory.doc.ic.ac.uk:/CLiCS/PPR2/papers/BucciarelliA-degpct.ps

[CGN94] R. L. Crole, S. J. Gay, and R. Nagarajan. An internal language for interaction categories. To appear in the Imperial College workshop on Theory and Formal Methods, 1994, 1994.

[CG] Roy L. Crole and Andrew D. Gordon. A sound metalogical semantics for input/output effects. In Computer Science Logic’94, Kazimierz, Poland, September 26–30, 1994. Proceedings to appear in Springer LNCS. AVAILABLE from theory.doc.ic.ac.uk:/CLiCS/PPR2/papers/soumsi.ps [CE94] Loïc Colson and Thomas Ehrhard, On Strong Stability and Higher order Sequentiality,

Ninth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, pag. 103–109, 1994. AVAILABLE from theory.doc.ic.ac.uk:/CLiCS/PPR2/papers/EhrhardT-strsho.ps

[CoqC93] Catarina Coquand. From semantics to rules: a machine assisted analysis. In Egon Börger, Yuri Gurevich, and Karl Meinke, editors, Proceedings of CSL ’93, LNCS 832, 1993. AVAILABLE from ftp.cs.chalmers.se:/pub/clics/catarina/nf.dvi

[Coq93] Th. Coquand. A Semantics of Evidence for Classical Arithmetic. to appear in the Journal of Symbolic Logic

[Coq94a] Thierry Coquand. A constructive topological proof of van der waerden’s theorem. Journal of Pure and Applied Algebra, 1994. To appear. AVAILABLE from ftp.cs.chalmers.se:/pub/clics/coquand/vanderw.dvi

[Coq94c] Thierry Coquand. A formal space of ultrafilters. Manuscript, August 1994. AVAILABLE from ftp.cs.chalmers.se:/pub/clics/coquand/ultraf.dvi

[Coq94d] Thierry Coquand. Infinite object in type theory. In Types for Proofs and Programs, International Workshop TYPES’93, LNCS 806, 1994.

[Cro94] R. L. Crole. Categories for Types. Cambridge University Press, 1994.

[DGR94] P. Degano, R. Gorrieri, and G. Rosolini. Graphs and event refinement. submitted. AVAILABLE from theory.ic.ac.uk:/papers/Rosolini/gref.ps

[DV94] M. Dawson and S.J. Vickers. Towards a GeoZ toolkit. In Hankin et al. [HMN94], pages ?–?

[Dyb94a] Peter Dybjer. A general notion of simultaneous inductive-recursive definition in type theory. Manuscript, April 1994. AVAILABLE from ftp.cs.chalmers.se:/pub/clics/peterd/Inductive Recursive.dvi

[Dyb94b] Peter Dybjer. Inductive families. Formal Aspects of Computing, 1994. To appear. AVAILABLE from ftp.cs.chalmers.se:/pub/clics/peterd/Inductive Families.dvi

[Dyb94c] Peter Dybjer. On the interpretation of coinductive types in intuitionistic type theory. Manuscript, September 1994. AVAILABLE from ftp.cs.chalmers.se:/pub/clics/peterd/Coinductive.dvi

[Dyb94d] Peter Dybjer. On the syntax of dependent types and the coherence problem. Manuscript, September 1994.

[EW94] Uffe H. Engberg and Glynn Winskel. Linear logic on Petri nets. Technical Report RS-94-3, February 1994. 54 pp. Appears in: Proceedings of REX ’93 (eds. J. W. de Bakker et al.), LNCS 803, 1994. AVAILABLE from ftp.daimi.aau.dk:/pub/BRICS/RS/94/3/BRICS-RS-94-3.ps

[Ehr93] Thomas Ehrhard, Projecting sequential algorithms on strongly stable functions, to appear in Annals of Pure and Applied Logic. AVAILABLE from theory.doc.ic.ac.uk:/CLiCS/PPR2/papers/EhrhardT-prosas.ps

[FH94] A. Fiech and M. Huth. Algebraic Domains of Natural Tranformations. Theoretical Computer Science, 1994. to appear. AVAILABLE from theory.doc.ic.ac.uk:/papers/Huth/adnt1.dvi and adnt2.dvi (figures)

[Fua] YuXi Fu. Categorical properties of logical frameworks. Submitted to Mathematical Structures in Computer Science. AVAILABLE from ftp.cs.man.ac.uk:/pub/applied logic/fuyuxi/CPLF.ps [Fuara] YuXi Fu. Encodings in polymorphism, revisited. Studia Logica, To appear.

AVAILABLE from ftp.cs.man.ac.uk:pub/applied logic/fuyuxi/polymorphism.ps

[Fuarb] YuXi Fu. Recursive models of general inductive types. Studia Logica, To appear. AVAILABLE from ftp.cs.man.ac.uk:/pub/applied logic/fuyuxi/rectypes.ps

[Fub] YuXi Fu. CZF in Martin-Löf’s type theory without identity types. Submitted to Theoretical Computer Science. AVAILABLE from ftp.cs.man.ac.uk:/pub/applied logic/fuyuxi/CZF.ps

[HB94] Graham Hutton and Carolyn Brown. Categories, allegories, and circuit design. Proc. IEEE symposium on Logic in Computer Science, July 1994, 1994.

[HJ94] C. Hermida and B. Jacobs. Fibrations with indeterminates: Contextual and functional completeness of polymorphic lambda calculi. Accepted for MSCS.

[HJK94a] M. Huth, A. Jung, and K. Keimel. Linear types and approximation. submitted to the Journal of MCSC, 1994. AVAILABLE from theory.doc.ic.ac.uk:/papers/Huth/lta.dvi

[HJK94b] M. Huth, A. Jung, and K. Keimel. Linear types, approximation, and topology. In Logic in Computer Science, pages 110–114. IEEE Computer Society Press, 1994.

[HMN94] C.L. Hankin, I.C. Mackie, and R. Nagarajan, editors. Theory and Formal Methods 1994: Proceedings of the Second Imperial College, Department of Computing, Workshop on Theory and Formal Methods, Workshops in Computing, Møller Center, Cambridge, UK, 11–14 September 1994. Springer-Verlag.

[HO93] J. M. E. Hyland and C.-H. L. Ong. Fair games and full completeness for Multiplicative Linear Logic without the mix-rule. preprint, 29 pages, 1993. AVAILABLE from theory.doc.ic.ac.uk:/papers/Ong/fcomplete.ps

[HO94] J. M. E. Hyland and C.-H. L. Ong. Dialogue games and innocent strategies: An approach to observational full abstraction for PCF. preprint, 89 pages, 1994. AVAILABLE from theory.doc.ic.ac.uk:/papers/Ong/dgis.ps

[HRa] B.P. Hilken and D.E. Rydeheard. Categories with computable structure. Submitted to Mathematical Structures in Computer Science. AVAILABLE from ftp.cs.man.ac.uk:/pub/applied logic/compos.ps

[HRb] B.P. Hilken and D.E. Rydeheard. A theory of classes: Proofs and models. Submitted to Mathematical Structures in Computer Science. AVAILABLE from ftp.cs.man.ac.uk:/pub/applied logic/classes.ps

[Haa94] C. Haack. A decomposition theorem for domains. Submitted, 1994. AVAILABLE from theory.doc.ic.ac.uk:/papers/Jung/decomp.ps

[Her93] Claudio Alberto Hermida. Fibrations, Logical Predicates and Indeterminates. PhD thesis, Department of Computer Science, University of Edinburgh, November 1993. Report DAIMI PB - 462, Computer Science Department, Aarhus University.

[Her94] Hugo Herbelin. A lambda-calculus structure isomorphic to sequent calculus structure. In paper accepted to CSL (Computer Science Logic), 1994. AVAILABLE from ftp.cs.chalmers.se:/pub/clics/herbelin/LJsubst.dvi

[Hil94] B. P. Hilken. Towards a proof theory of rewriting: the simply-typed 2-λ-calculus. Technical Report 336, University of Cambridge Computer Laboratory, 1994. Journal version submitted. AVAILABLE from theory.doc.ic.ac.uk:/CLiCS/PPR2/papers/twolambda.ps [Hut94a] M. Huth. Interaction Orders as Games. In C. Hankin and R. Nagarajan, editors, Theory

and Formal Methods 1994, Workshops in Computing. Springer Verlag, 1994. to appear.

[Hut94b] M. Huth. Functional Bisimulation. submitted to the special issue of TCS commemorating the workshop on Semantics and Completion in Chartres, France, November 1993, 1994. AVAILABLE from theory.doc.ic.ac.uk:/papers/Huth/fb.dvi

[Hut94c] M. Huth. Interaction Orders as Games. Technical Report 1639, Technische Hochschule Darmstadt, 1994. AVAILABLE from theory.doc.ic.ac.uk:/papers/Huth/iog.dvi

[Hut94d] M. Huth. Linear Domains and Linear Maps. In S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Mathematical Foundations of Programming Semantics, volume 802 of Lecture Notes in Computer Science, pages 438–453. Springer Verlag, 1994. AVAILABLE from theory.doc.ic.ac.uk:/papers/Huth/ldlm.dvi

[Hut94e] M. Huth. A maximal monoidal closed category of distributive algebraic domains. Information and Computation, 1994. To appear. AVAILABLE from theory.doc.ic.ac.uk:/papers/Huth/mmccfinalversion.dvi

[Hut94f] M. Huth. Zero Dimensional and Connected Domains. Semigroup Forum, 1994. to appear. AVAILABLE from theory.doc.ic.ac.uk:/papers/Huth/zd.dvi

[JNW94] André Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from open maps. BRICS Technical Report RS-94-7, May 1994. 42 pp. Journal version of LICS ’93 paper. AVAILABLE from ftp.daimi.aau.dk:/pub/BRICS/RS/94/7/BRICS-RS-94-7.ps

[KP94] K. Keimel and J. Paseka. A direct proof of the Hofmann-Mislove theorem. Proceedings of the AMS, 120:301–303, 1994.

[Laf93] Yves Lafont A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier), to appear in Journal of Pure and Applied Algebra (North Holland). AVAILABLE from lmd.univ-mrs.fr:/pub/lafont/finiteness.ps

[Laf94] Yves Lafont From Proof-Nets to Interaction Nets, to appear in the proceedings of the Linear Logic Workshop (Cornell, 1993). AVAILABLE from lmd.univ-mrs.fr:/pub/lafont/proofnets.ps

[Laf94a] Yves Lafont Equational Reasoning with 2-dimensional Diagrams, to appear in the proceedings of a summer school on rewriting (Font-Romeu 93, LNCS, Springer-verlag). AVAILABLE from lmd.univ-mrs.fr:/pub/lafont/equational.ps

[MH94] Erik Meijer and Graham Hutton. Fold and unfold simplified and extended (working title). Work in progress, Utrecht University and Chalmers University, 1994.

[Mog94a] E. Moggi. A general semantics for evaluation logic. In 9th LICS Conference. IEEE, 1994. AVAILABLE from theory.ic.ac.uk:/papers/Moggi/elt3.ps

[Mog94b] E. Moggi. Representing V T LoE in evaluation logic. 1994. AVAILABLE from theory.ic.ac.uk:/papers/Moggi/elt-vtloe.ps

[NdPR94] Monica Nesi, Valeria de Paiva, and Eike Ritter. Rewriting properties of combinators for intuitionistic linear logic. In Proceedings of the Workshop on Higher Order Algebra, Logic and Term Rewriting. To appear in Lecture Notes in Computer Science, Berlin, Heidelberg, New York, 1994. AVAILABLE from theory.doc.ic.ac.uk:/papers/Ritter/hoa93.ps [OR94] Luke Ong and Eike Ritter. A Generic Strong Normalization Argument: Application

to the Calculus of Constructions. Lecture Notes in Computer Science No. 832, Berlin, Heidelberg, New York, 1994. AVAILABLE from theory.doc.ic.ac.uk:/papers/Ong/csl93.ps

[Ong94] C.-H. L. Ong. Correspondence between operational and denotational semantics: the full abstraction problem for PCF. In S. Abramsky, D. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, Vol 4. Oxford Univ. Press, 1994. To appear. AVAILABLE from theory.doc.ic.ac.uk:/papers/Ong/handbook.ps

[PW94] Gordon Plotkin and Glynn Winskel. Bistructures, bidomains and linear logic. BRICS Technical Report RS-94-9, May 1994. 16 pp. Appears in the proceedings of ICALP ’94, LNCS, 1994. AVAILABLE from ftp.daimi.aau.dk:/pub/BRICS/RS/94/9/BRICS-RS-94-9.ps

[Pit93] A. M. Pitts. Relational properties of domains. Technical Report 321, Cambridge Univ. Computer Laboratory, December 1993. 37 pages. AVAILABLE from theory.doc.ic.ac.uk:/papers/Pitts/relpd.ps

[Pit94a] A. M. Pitts. Categorical logic. A chapter of Volume XI of the Handbook of Logic in Computer Science (S. Abramsky, D. M. Gabbay and T. S. Maibaum, eds), to appear., April 1994. AVAILABLE from theory.doc.ic.ac.uk:/papers/Pitts/CLICS/cambridge/CLchapter.ps

[Pit94b] A. M. Pitts. A co-induction principle for recursively defined domains. Theoretical Computer Science, 124:195–219, 1994. AVAILABLE from theory.doc.ic.ac.uk:/papers/Pitts/coiprd.ps

[Pit94c] A. M. Pitts. Computational adequacy via ‘mixed’ inductive definitions. In Mathematical Foundations of Programming Semantics, Proc. 9th Int. Conf., New Orleans, LA, USA, April 1993, volume 802 of Lecture Notes in Computer Science, pages 72–82. Springer-Verlag, Berlin, 1994. AVAILABLE from theory.doc.ic.ac.uk:/papers/Pitts/compavm.ps

[RR94] E.P. Robinson and G. Rosolini. Reflexive graphs and parametric polymorphism. In S. Abramsky, editor, Proc. 9th Symposium in Logic in Computer Science, pages 364– 371, Paris, 1994. I.E.E.E. Computer Society. AVAILABLE from theory.ic.ac.uk:/papers/Rosolini/reflpar.ps

[Rit94a] Eike Ritter. Normalization for typed lambda calculi with explicit substitution. In Proceedings of the 1993 Annual Conference of the European Association for Computer Science Logic, pages 295–304. Lecture Notes in Computer Science No. 832, Berlin, Heidelberg, New York, 1994. AVAILABLE from theory.doc.ic.ac.uk:/papers/Ritter/substsn.ps

[Rit94b] Eike Ritter. Categorical abstract machines for higher-order lambda calculi. Theoretical Computer Science, to appear 1994. AVAILABLE from theory.doc.ic.ac.uk:/papers/Ritter/mfps92.ps

[Rob94a] E.P. Robinson. A note on the presentation of enriched monads. August 1994. AVAILABLE from theory.ic.ac.uk:/papers/Robinson/general-monads.dvi

[Rob94b] E.P. Robinson. Variations on algebra: monadicity and generalisations of equational theories. Computer Science Technical Report 6/94, University of Sussex, April 1994. (submitted to Mathematical Structures in Computer Science).

[Ros94] G. Rosolini. Synthetic Domain Theory. draft. Genova, 1994. AVAILABLE from theory.ic.ac.uk:/papers/Rosolini/notes sdt.ps [Sim94a] H. Simmons. The glueing construction and lax limits. Mathematical Structures in

Computer Science, 1994. 40 pages.

[Sim94b] H. Simmons. The monotonous elimination of predicate variables. J of Logic and Computation, 1994. 45 pages.

[Sima] H. Simmons. Axiomatic substitution. Preprint. Available on from the Dept of Computer Science, University of Manchester.

[Simb] H. Simmons. A density property of the primitive recursive degrees. Submitted to Theoretical Computer Science, 1994.

[Simc] H. Simmons. Ordered structures, topologies and duality. Preprint: Lecture Notes. AVAILABLE from ftp.cs.man.ac.uk:pub/applied logic/dualities.ps

[Simd] H. Simmons. Program extraction by the Leivant method. Preprint. Available on from the Dept of Computer Science, University of Manchester.

[Sime] H. Simmons. Taking the Curry-Howard correspondence seriously. Preprint: Lecture Notes (134 pages). AVAILABLE from ftp.cs.man.ac.uk:/pub/applied logic/logic-and-comp.ps

[Sta] Ian Stark. Categorical models for local names. Lisp and Symbolic Computation. To appear. AVAILABLE from theory.doc.ic.ac.uk:/CLiCS/PPR2/papers/catmln.ps

[Sün92] Ph. Sünderhauf. Quasi-uniform completeness in terms of Cauchy nets. Technical Report 1529, Technische Hochschule Darmstadt, 1992. 8 pp.

[Sün93] Ph. Sünderhauf. Constructing a quasi-uniform function space. Technical Report 1541, Technische Hochschule Darmstadt, 1993. 26 pp.

[Sün94a] Ph. Sünderhauf. Discrete Approximation of Spaces. PhD thesis, Technische Hochschule Darmstadt, 1994. 91 pp. AVAILABLE from theory.doc.ic.ac.uk:/papers/Jung/discrete.ps

[Sün94b] Ph. Sünderhauf. A faithful computational model of the real numbers. Technical Report 1610, Technische Hochschule Darmstadt, 1994. 17 pp. AVAILABLE from theory.doc.ic.ac.uk:/papers/Jung/reals.ps

[Tay94] Paul Taylor. Intuitionistic sets and ordinals. 1994.

[Tay95] Paul Taylor. Practical Foundations. Cambridge University Press (?), 1995? (In preparation).

[Vic92] Steven J. Vickers. Topical categories of domains. In Winskel, editor, Proceedings of the CLICS workshop, Aarhus, pages 261–274, 1992. Technical report DAIMI PB–397–I, Computer Science Department, Aarhus University.

[Vic93] Steven J. Vickers. Geometric logic in computer science. In Ryan Burn, Gay, editor, Theory and Formal Methods 1993, Workshops in Computing, pages 37–54. Springer-Verlag, 1993.

[Vic94a] S.J. Vickers. Geometric logic as a specification language. In Hankin et al. [HMN94], pages ?–?

[Vic94b] S.J. Vickers. Locales are not pointless. In Hankin et al. [HMN94], pages ?–?

[Win94] Glynn Winskel. Stable bistructure models of PCF. BRICS Technical Report RS-94-13, May 1994. 26 pp. Preliminary draft. Invited lecture for MFCS ’94. To appear in the proceedings of MFCS ’94, LNCS, 1994. AVAILABLE from ftp.daimi.aau.dk:/pub/BRICS/RS/94/13/BRICS-RS-94-13.ps