March 2004 - Categories - categories.org.au

Topos cohomology, context and technical questions
by Colin McLarty 16 Apr '04

16 Apr '04

Thanks to Christopher Townsend and Carsten Butz for help on cohomology in an elementary topos. It seems the general theory is not much advanced beyond what it was in Johnstone 1977. My question came out of a conversation with algebraic geometers several years ago, which I have taken up again lately. Deligne, for example, describes toposes as one of Grothendieck's great ideas (one of Grothendieck's four "idees maitresses"). But for him and many other geometers their value lies in organizing cohomology. Insofar as Grothendieck toposes support a simple general theory of cohomology, and elementary toposes do not, these people find only Grothendieck toposes interesting. Certainly there is a lot to say for elementary topos theory even from that perspective: The elementary topos axioms organize the theory of Grothendieck toposes. Elementary toposes have some cohomology theory though not so simple and general. And elementary toposes have other roles. What interests me, now, is how far elementary topos theory helps with cohomology per se. One approach is to notice: The elementary theory of "a topos whose Abelian groups have enough injectives" supports a considerable general theory of cohomology via injective resolutions. But I have not worked out how far it really goes. (People with foundational interests will notice the exact result depends on whether and how this theory works with infinite complexes. There are various approaches depending on what you mean by "elementary".) This raises my first technical question: SGA 4 proves inverse image functors preserve flat modules, but the transparent proof assumes enough points (Exp. V Prop. 1.7). Deligne gives a far from transparent proof, for all (Grothendieck) toposes, in an appendix on "local inductive limits". He urges the reader "to avoid, as a matter of principle, reading this appendix". Is the result proved more simply somewhere? Do "local inductive limits" survive today in some form? In short, can we follow Deligne's advice on not reading this appendix, and still prove his result? I have made no progress on the appendix yet, as the opening definition is full of typos. If there is a cleaner exposition I'd rather start with that. The second question: The IHES version of SGA 4 gives a faulty proof that, in every (Grothendieck) topos, rings admit a standard kind of resolution over any cover by tensoring with a resolution of the integers. This is Prop. 1.4 of Expose V. The Springer-Verlag version corrects the mistake by proving the result only when the topos has enough points (Prop 1.11 Exp. V). Johnstone 1977 recovers the theorem for the case of a presheaf topos (Lemma 8.2) which is the case of interest and easily extends to any topos with enough points. Is that version optimal, in some easy to prove sense? Is there an easy example of a ring in a Grothendieck topos where the resolution fails? Is it known to be optimal in any sense? best, Colin

2 1

arithmetical and geometric reals in (models of) SDG
by Thomas Streicher 11 Apr '04

11 Apr '04

Recently I was asking myself what is the relation between the arithmetical (Dedekind) reals in a topos and a ring R satisfying the usual SDG axioms (i.e. at least the Kock-Lawvere) axiom. >>From the few things I know about models of SDG it seems to me as if in the usual sheaf models (over a site Loc of `loci') the Dedekind reals form a subring of R = y(\Re) (where \Re is the locus corresponding to the reals). As long as one considers just presheaves that's clear as the Dedekind reals are given by \Delta(\Re). Probably taking sheaves that situation isn't changed dramatically? So my impression is that in the usual sheaf models of SDG the real line R carries the structure of an algebra over the Dedekind reals. However, I don't see how to construct such an embedding of Dedekind reals into R based only on the usual axioms of SDG. Of course, when given an order on R and R is assumed as a Q-algebra then one has a good candidate for a function from R to R_D sending x \in R to {q \in Q | q.1 \leq x}. But how to define purely logically an embedding of R_D into R remains mysterious (to me). I am fully aware of the fact that my question is a bit `against the strain' of SDG but we know that both kinds of reals do coexist in topos models. But is this coexistence only peaceful or rather more collaborative? I am certain that people must have thought about this but I couldn't find anything at the usual places where to look. So I would be grateful for comments (on the correctness of my above speculations) or pointers to existing literature or folklore. Best, Thomas Streicher

3 2

on the axiom of infinity
by Peter Freyd 01 Apr '04

01 Apr '04

Let *T* be the topos freely generated by its constants (a few postings ago I called it the initial object in the category of topoi and logical morphisms), let Omega be its subobject classifier and let P denote Omega^Omega. I wrote: There's a subobject, M, of P on which we may define the structure of a rig (a ring without negation) that mimics the natural numbers. In particular the set of global sections, that is, maps from 1 to M with its inherited rig structure, is isomorphic to the standard natural numbers... [Moreover we may] construct a topos-object in *T* whose topos of global sections is isomorphic to the free topos with NNO. And, as for M, an equation in the theory of topoi is internally true for this internal topos iff it is true for the free topos with NNO. It occurs to me that the proofs I have in mind rest on at least three considerations that may not be well known. (I have no idea about other proofs.) The first consideration stems from curiosity about the complete algebraic theory of Omega. In particular, what are its unary operators? Some would phrase that: What are the "modalities" implicit in higher-order intuitionistic logic? There's a particular operator that keeps popping up for me. In an arbitrary heyting algebra define x << y to mean that not only is x less than or equal to y, but the value of y -> x is as small as it can be, that is, y -> x = x. In a complete heyting algebra define an order-preserving, inflationary unary operation s by sx = inf{ y | x << y }. E.g.: on a linearly ordered set if { y | x < y } has a least element then that's what sx is. If there is no smallest element above x, then sx = x (even without the completeness hypothesis). In particular, note, there no assertion that x << sx. The subobject classifier in an elementary topos is complete in the relevant sense: s is definable. A quick description of the construction to follow is that we're going to turn s into the successor operation on an NNO. DIVERSION: The definition I just gave is the first I came across. The next incarnation for me was when I wanted a measure of the failure of booleaness. In any topos, *A*, there's a largest subterminator B with the property that the slice category *A*/B is boolean. But given any subterminator, U, we have its "closed sheaves", *A*_(U), the full subcat of objects A such that AxU --> U is an iso. (This is a subcategory of sheaves for a Lawvere-Tierney topology. Starting with a space X then Sheaves(X)_(U) may be identified with Sheaves(U'), where U' denotes the complement of U.) Note that the lattice of subterminators in *A*_(U) is isomorphic to the interval of subterminators in *A* from U up. We can define BU to be the largest subterminator in *A*_(U) such that *A*_(U)/BU is boolean. The interval of subterminators in *A* from U up to BU is boolean and in the relevant internal sense, BU is the largest such subterminator. We can, of course, translate this all to a unary operation on Omega. It's the same operator s. When one specializes this to a space X it becomes historically familiar if we dualize it it to a deflationary operator on closed subsets. It's the operation that removes isolated points. The very operation that got Cantor started. Hence the word "historically". END OF DIVERSION Back to *T*: in the monoid Omega^Omega define C to be the submonoid generated by s. We're going to use 0 : 1 --> C to denote the name of the identity element (you might think of it as s^0) and we're going to use suc : C -> C to denote the function that sends an element x to sx. It's easy to verify that the necessary and sufficient condition for C,0,suc to be an NNO is that -- in the internal sense -- it has no fixed points. The argument works for any one-generator partially- ordered monoid whose identity element is below the generator. Let E be the equalizer of 1, suc : C --> C. I'm saying that C,0,suc is an NNO iff E is empty. Let V be the negation of the image of E --> 1. It is the largest subterminator such that C,0,suc becomes an NNO in the slice category *T*/V. Now for the nice part. The sconing argument tells us that V, as is the case for any non-trivial negation, is an indecomposable projective -- that is, the covariant functor represented by V is an exact functor. And that means that 1 is an indecomposable projective in the slice category *T*/V. The "global-section" functor from *T*/V to *Sets* is exact. Hence (by my first theorem in this subject) it preserves the NNO and all the definable structure thereon. I advertised an object, not in a slice category but in *T*. So define M = C^V. Then it is easily verified that the global sections of M as defined in *T* are naturally isomorphic to the global sections of C/V as defined in *T*/V. Since it has an NNO we can construct all sorts of things in *T*/V. We'll settle here for the free-topos-object-with-NNO. That is, there is an object T in *T*/V with a binary partial operation that serves as the free topos with NNO in *T*/V. Since the global-section functor is exact we know that it preserves free structures in great generality (part of lore of exact functors between topoi). In particular it carries T to a standard free topos with NNO .And, finally, we know that T^V has that same last property as an object in *T*. (Better, actually, is to take T to be the free topos on one object. Every finitely presented topos is a slice thereof -- including the free-topos-with-NNO.) Surely this is all too easy. Yeah. I skipped over something. My point about negations being indecomposable projectives requires them to be non-trivial. (The covariant functor represented by 0 is not exact; it does not preserve the coterminator.) That is, we need to show that V is not 0. But for that it suffices (given the defining universal property for *T*) to show in at least one topos that the recipe for V yields something nontrivial. Equivalently, we need a topos in which V = 1. The most easily named example is the topos of N-sets, or as I described it a few postings ago, the topos of sets with distinguished self-maps. This topos is two-valued, that is, Sub(1) has just two elements and that can be an advantage. (We know that we must show that suc : C --> C has no fixed points.) In fact, I find it easier to work in the slice category (*Sets*^N)/N. (There is, anyway, a faithful representation of *Sets*^N into (*Sets*^N)/N.) The category (*Sets*^N)/N is equivalent to the category of covariant set-valued functors on the poset also denoted N. The advantage here is just the opposite: (*Sets*^N)/N is generated by its non-zero subterminators and they're all indecomposable projectives. DIVERSION: When I first finished writing this piece I noticed for the first time that there's a historically much better example. Take the category of sheaves on the reals (or for that matter, any space of geometric interest). Then follow in Cantor's footsteps. FOOTNOTE: One variation worth mentioning. Instead of taking C as the submonoid generated by s take it to be the smallest up-closed submonoid, that is, this new version of C will be closed with respect to sups. This C is trying to be a big ordinal number. Indeed, following just the path first taken by Cantor we can find Grothendieck topoi where C looks like an arbitrarily large initial section of ordinals. In the free topos with NNO this C seems to be none other than the ordinal (in some relevant sense) of all recursively enumerable ordinals.

3 2

New paper on Profunctors, Open Maps and Bisimulation
by gianluca.cattani 31 Mar '04

31 Mar '04

This is to announce the availability of the following paper Profunctors, Open Maps and Bisimulation by Gian Luca Cattani and Glynn Winskel. The paper can be downloaded in postscript version from http://www.cl.cam.ac.uk/~gw104. Regards, Gian Luca Cattani

1 0

CONCUR 2004: Final CFP - deadline approaching
by Concur 2004 30 Mar '04

30 Mar '04

Final Call for Papers for CONCUR 2004 [Apologies for multiple postings] The submission deadline for CONCUR 2004 is fast approaching: **** Friday 9 April 2004 **** New information since previous announcements: * David Harel (Weizmann Institute) will give an invited talk entitled "A Grand Challenge: Towards Full Reactive Modeling of a Multi-Cellular Animal" (see below for other invited speakers) * There will be a special issue of the journal Theoretical Computer Science associated with CONCUR 2004. * There will be a volume of Electronic Notes in Theoretical Computer Science associated with the workshops. ------------------------------------------------- CONCUR 2004, the 15th International Conference on Concurrency Theory, takes place at the Royal Society, London, Tuesday 31 August - Friday 3 September 2004. As well as the main event, we will also hold many workshops on Monday 30th August and Saturday 4th February, as detailed below. Further information is available at the conference's web site http://www.doc.ic.ac.uk/concur2004 Important dates Submission: Friday 9 April 2004 Notification: Monday 31 May 2004 Final version: Tuesday 15 June 2004 The purpose of the CONCUR conferences is to bring together researchers, developers and students in order to advance the theory of concurrency, and promote its applications. Interest in this topic is continuously growing, as a consequence of the importance and ubiquity of concurrent systems and their applications, and of the scientific relevance of their foundations. Submissions are solicited in all areas of semantics, logics and verification techniques for concurrent systems. Principal topics include (but are not limited to): - Basic models and logics of concurrent and distributed computation (such as process algebras, Petri nets, domain theoretic or game theoretic models, modal and temporal logics). - Specialized or enriched models (such as circuits, synchronous systems, real time and hybrid systems, stochastic systems, data bases, mobile and migrating systems, parametric protocols, security protocols). - Related verification techniques and tools (such as state-space exploration, model-checking, synthesis, abstraction, automated deduction, testing). - Related programming models (such as distributed, constraints or object oriented, graph rewriting, as well as associated type systems, static analyses, abstract machines, and environments). Authors are invited to submit an extended abstract not exceeding 15 pages electronically via the web submission form at the conference's web site. Submissions will be evaluated by the program committee for inclusion in the proceedings, which will be published by Springer-Verlag in the Lecture Notes in Computer Science series. Papers must contain original contributions, be clearly written, and include appropriate reference to and comparison with related work. Simultaneous submissions to other conferences are not allowed. There will be a special issue of the journal Theoretical Computer Science associated with Concur 2004. Invited speakers * David Harel (Weizmann Institute): Invited Talk entitled "A Grand Challenge: Towards Full Reactive Modeling of a Multi-Cellular Animal" * Sriram K. Rajamani (Microsoft Research): Invited Talk on Zing (a model-checking tool based on ideas from process algebra) * Peter O'Hearn (Queen Mary University of London) and Steve Brookes (Carnegie-Mellon): Tutorial on Local Reasoning about Concurrent Imperative Programs * Bengt Jonsson (Uppsala): Tutorial on Regular Model Checking Organisers * General chair: Philippa Gardner * Programme Committee co-chairs: Philippa Gardner, Nobuko Yoshida * Workshops organisers: Vladimiro Sassone, Julian Rathke * Local organisers: Iain Phillips, Sergio Maffeis, Alex Ahern Program committee Philippa Gardner, co-chair, UK Nobuko Yoshida, co-chair, UK Luca Aceto, Denmark Bruno Blanchet, Germany/France Steve Brookes, USA Luca De Alfaro, USA Paul Gastin, France Petr Jancar, Czech Republic Joost-Pieter Katoen, Netherlands Dietrich Kuske, Germany Cosimo Laneve, Italy Michael Mendler, Germany Ugo Montanari, Italy Catuscia Palamidessi, France Vladimiro Sassone, UK PS Thiagarajan, Singapore Antti Valmari, Finland Wang Yi, Sweden Concur 2004 gratefully acknowledges sponsorship from Microsoft Research. Monday workshops - Workshop on Structural Operational Semantics, SOS 2004 URL = http://www.cs.auc.dk/~luca/SOS-WORKSHOP Contact = Luca Aceto <luca(a)cs.auc.dk> - 11th International Workshop in Expressiveness in Concurrency, EXPRESS 2004 URL = http://www.win.tue.nl/express04 Contact = Flavio Corradini <flavio.corradini(a)unicam.it> - II Workshop on Object-Oriented Developments, WOOD 2004 URL = http://www.dsi.unive.it/wood2004 Contact = Viviana Bono <bono(a)di.unito.it> - 3rd International Workshop on Foundations of Coordination Languages and Software Architectures, FOCLASA 2004 URL = http://www.info.fundp.ac.be/~jmj/Foclasa04 Contact = Jean-Marie JACQUET <jmj(a)info.fundp.ac.be> - 2nd International Workshop on Security Issues in Coordination Models, Languages and Systems, SECCO 2004 URL = http://www.cs.unibo.it/secco04/ Contact = Gianluigi Zavattaro <zavattar(a)cs.unibo.it> - BIOCONCUR 2004 URL = http://www.imm.dtu.dk/bioconcur04 Contact = Anna Ingolfsdottir <annai(a)decode.is> Friday afternoon + Saturday - Global Ubiquitous Computing URL = http://www.cogs.susx.ac.uk/fgc04 Contact = Julian Rathke <julianr(a)susx.ac.uk> Saturday workshops - 3rd International Workshop on Parallel and Distributed Methods in VerifiCation, PDMC 2004 URL = http://www.fi.muni.cz/~brim/PDMC04/ Contact = Martin Leucker <Martin.Leucker(a)it.uu.se> - First International Workshop on Practical Applications of Stochastic Modelling, PASM 2004 URL = http://www.doc.ic.ac.uk/pasm2004 Contact = Jeremy Bradley <jb(a)doc.ic.ac.uk> - Infinity URL = http://www.lfcs.ed.ac.uk/Infinity04 Contact = Julian Bradfield <jcb(a)inf.ed.ac.uk> - Fourth International Workshop on Automated Verification of Critical Systems, AVoCS 2004 URL = http://www.doc.ic.ac.uk/~mrh/AVoCS04.html Contact = Michael Huth <mrh(a)doc.ic.ac.uk> * There will be a volume of Electronic Notes in Theoretical Computer Science associated with the workshops.

1 0

Postscript^2
by Peter Freyd 27 Mar '04

27 Mar '04

Cats & Alligators has just made it into Neil Sloane's "On-Line Encyclopedia of Integer Sequences"! Here's how the top of A001037 now reads: ID Number: A001037 (Formerly M0116 and N0046) URL: http://www.research.att.com/projects/OEIS?Anum=A001037 Sequence: 1,2,1,2,3,6,9,18,30,56,99,186,335,630,1161,2182,4080,7710, 14532,27594,52377,99858,190557,364722,698870,1342176, 2580795,4971008,9586395,18512790,35790267,69273666, 134215680,260300986,505286415,981706806 Name: Degree n irreducible polynomials over GF(2); n-bead necklaces with beads of 2 colors when turning over is not allowed and with primitive period n; binary Lyndon words of length n. Comments: Also dimensions of free Lie algebras - see A059966, which is essentially the same sequence. References E. R. Berlekamp, Algebraic Coding Theory, McGraw-Hill, NY, 1968, p. 84. R. Church, Tables of irreducible polynomials for the first four prime moduli, Annals Math., 36 (1935), 198-209. P. J. Freyd and A. Scedrov, Categories, Allegories, North-Holland, Amsterdam, 1990. See 1.925. E. N. Gilbert and J. Riordan, Symmetry types of periodic sequences, Illinois J. Math., 5 (1961), 657-665. M. A. Harrison, On the classification of Boolean functions by the general linear and affine groups, J. Soc. Indust. Appl. Math. 12 (1964) 285-299. M. Lothaire, Combinatorics on Words. Addison-Wesley, Reading, MA, 1983, p. 79. G. Melancon, Factorizing infinite words using Maple, MapleTech journal, vol 4, no. 1, 1997, pp. 34-42, esp. p. 36. M. R. Nester, (1999). Mathematical investigations of some plant interaction designs. PhD Thesis. University of Queensland, Brisbane, Australia. G. Viennot, Algebres de Lie Libres et Monoides Libres, Lecture Notes in Mathematics 691, Springer verlag 1978. Postscript^3: For the record, this is the 8th item in which my name appears. The complete list: A000602 A000628 A000670 A001037 A067608 A067609 A067610 A067765

1 0

Addendum
by Peter Freyd 26 Mar '04

26 Mar '04

I wrote: [I]n the category of N-sets (sets with a distinguished self-map) let A be the two-element set in which the distinguished self-map has a unique fixed point....A^A, the object of self-maps of A, falls apart as a coproduct (disjoint union) of continuously many N-sets. Hence if one takes the set of equivalence classes of A^A, where the equivalence relation is the double-negation of equality, one obtains a discrete set (it has trivial N-action) whose cardinality is the continuum. It's more complicated. One obtains a disjoint union of "cycles", that is, objects of the form Z/nZ where the distinguished self-map is addition by 1. For each n > 0 there are only a finite number of copies of Z/nZ. The number of copies of Z = Z/0Z is uncountable. Postscript: The sequence of numbers of copies of each finite cycle is, of course, guaranteed to be in Neil Sloan's "On-Line Encyclopedia of Integer Sequences", but we didn't have that. Instead in 1.925 of Cats & Alligators we gave a ridiculous -- but both correct and unimprovable -- formula for that finite number. Preceding it was a sentence that begins "Bearing in mind that, as far as we know, this is computation for its own sake". Anyway, you can find the same formula at mathworld.wolfram.com/IrreduciblePolynomial.html under the name L_q(n) (with q = 2). With the exception of the zero'th value (in our case it's 2^{\Aleph_0}, for Lyndon words it's 1) here's what Sloan has to say: ID Number: A001037 (Formerly M0116 and N0046) URL: http://www.research.att.com/projects/OEIS?Anum=A001037 Sequence: 1,2,1,2,3,6,9,18,30,56,99,186,335,630,1161,2182,4080,7710, 14532,27594,52377,99858,190557,364722,698870,1342176, 2580795,4971008,9586395,18512790,35790267,69273666, 134215680,260300986,505286415,981706806 Name: Degree n irreducible polynomials over GF(2); n-bead necklaces with beads of 2 colors when turning over is not allowed and with primitive period n; binary Lyndon words of length n. Comments: Also dimensions of free Lie algebras - see A059966, which is essentially the same sequence. References E. R. Berlekamp, Algebraic Coding Theory, McGraw-Hill, NY, 1968, p. 84. R. Church, Tables of irreducible polynomials for the first four prime moduli, Annals Math., 36 (1935), 198-209. E. N. Gilbert and J. Riordan, Symmetry types of periodic sequences, Illinois J. Math., 5 (1961), 657-665. M. A. Harrison, On the classification of Boolean functions by the general linear and affine groups, J. Soc. Indust. Appl. Math. 12 (1964) 285-299. M. Lothaire, Combinatorics on Words. Addison-Wesley, Reading, MA, 1983, p. 79. G. Melancon, Factorizing infinite words using Maple, MapleTech journal, vol 4, no. 1, 1997, pp. 34-42, esp. p. 36. M. R. Nester, (1999). Mathematical investigations of some plant interaction designs. PhD Thesis. University of Queensland, Brisbane, Australia. G. Viennot, Algebres de Lie Libres et Monoides Libres, Lecture Notes in Mathematics 691, Springer verlag 1978.

1 0

University Lectureship in Computer Science, Univ of Oxford
by Luke Ong 26 Mar '04

26 Mar '04

UNIVERSITY OF OXFORD Mathematical and Physical Sciences Division Computing Laboratory in association with St John's College UNIVERSITY LECTURERSHIP IN COMPUTER SCIENCE Applications are invited for a University Lecturership in Computer Science from outstanding candidates working in any area of Computer Science. The successful candidate will be expected to engage in research of an internationally leading quality. He or she will be expected to lecture, supervise graduate students and perform other departmental duties under the direction of the Head of Department. The successful candidate will be appointed to a Tutorial Fellowship at St. John's College. As a Tutorial Fellow, the appointee will be expected to take a full part in the selection, academic progress and pastoral oversight of undergraduates reading Final Honours Schools involving Computer Science. The college requires a maximum of 6 hours teaching per week of full term (averaged over the three terms of the academic year) and performance of associated duties such as the pastoral care of Computer Science graduates. The combined University and College salary will be according to age on a scale up to £42,900 (pay award pending). Further allowances may be payable from the college as detailed in its associated Further Particulars. Further Particulars of the post, including Selection Criteria and application method, together with more detailed descriptions of the Department and College duties are available at www.comlab.ox.ac.uk/jobs by telephone request to +44 (0)1865 273831 or by email request to lecturership(a)comlab.ox.ac.uk. The closing date for receipt of applications is 21st April 2004.

1 0

Cantor set/cantor dust and constructivism
by Galchin Vasili 24 Mar '04

24 Mar '04

Hello, This question is a little bit afield; however, it is still tied in with intuitionistic logic. On my Linux machine, I have a screensaver that is a three-dimensional of a Cantor set. A Cantor set has prescription or algorithm as to how we "calculate" or build it. Question: From a constructivist viewpoint though, can we ever realize the actual object which is infinite? Regards, Bill Halchin

2 1

Domains VII (Call for Abstracts)
by Thomas Streicher 24 Mar '04

24 Mar '04

Announcement and Call for Abstracts DOMAINS VII Darmstadt, August 29 - September 1 The WORKSHOP DOMAINS series is aimed at computer scientists and mathematicians alike who share an interest in the mathematical foundations of computation. It focusses on domains, their applications and related topics. The series was conceived and first realised by Klaus Keimel in Darmstadt in 1994. This seventh workshop returns to Darmstadt on the occasion of his 65th birthday. The following have declared their intention to participate: P.-L. Curien Univerity Paris 7 Yu.L. Ershov Sib. Branch of the Russian Academy of Science, Novosibirsk J.D. Lawson Louisiana State University M. Mislove Tulane University J.-E. Pin University Paris 7 D.S. Scott Carnegie Mellon University SCOPE Domain Theory has had applications to programming language semantics and logics (lambda calculus, PCF, LCF), recursion theory, general topology, topological algebra and analysis. As such Domain Theory is highly interdisciplinary. Part of the workshop will be devoted to the study of Continuous Phenomena in Computer Science, one of the themes of the APPLIED SEMANTICS II Network. Topics of interaction with Domain Theory for this workshop include, but are not limited to computation over the reals and other classical spaces probabilistic computation topology / locale theory constructive mathematics and its semantics computability theory program semantics program logics lambda calculus models of sequential computation LOCATION The Workshop will take place at Technische Universitaet Darmstadt located in the center of the city of Darmstadt. WORKSHOP SCHEDULE August 29 is the arrival day. There will be a barbecue in the afternoon or a dinner in the evening. The talks will take place from 9 a.m on Monday, August 30, until 5 p.m. on Wednesday, September 1. PARTICIPATION If you would like to participate in this workshop as we hope, please let us know: email: domains7(a)mathematik.tu-darmstadt.de Please indicate whether you would like to give a talk. SUBMISSION of ABSTRACTS One page abstracts should be submitted to domains7(a)mathematik.tu-darmstadt.de Shortly after an abstract is submitted (usually one or two weeks), the authors will be notified by the programme committee. Abstracts will be dealt with on a first come/first served basis. Submit as soon as possible, DEADLINE 30 June 2004 ACCOMODATION Participants will have to arrange accomodation by themselves in local hotels. There will be a certain number of hotel rooms made available through www.proregio-darmstadt.de. Details will be communicated later. FEES The Workshop is organized without institutional financial support. There will be a modest registration fee for covering expenses. PROGRAMME AND ORGANIZING COMMITTEE Achim Jung University of Birmingham Klaus Keimel Technische Universitaet Darmstadt Thomas Streicher Technische Universitaet Darmstadt

1 0