March 1999 - Categories - categories.org.au

WAIT99 - Call for Papers
by Gabriel Baum 19 Apr '99

19 Apr '99

Please find below the WAIT'99 Call for Papers. We apologize if you receive this message more than once. Call for Papers 28 JAIIO - WAIT'99 Argentinian Workshop on Theoretical Computer Science Buenos Aires - Argentina September 6-7, 1999 ---------------------------------------------------------------------------- --------- The 3rd Argentinian Workshop on Theoretical Computer Science (WAIT'99) will be part on the 28th Argentinean Conference on Informatics and Operations Research (28 JAIIO), to be held in Buenos Aires from September 6th to September 10th, 1999. The goal of the workshop is bringing together researchers from academy (from Argentinean and other universities) and industry professionals in order to discuss theoretical, empirical and experimental results on the field of theoretical computer science. This workshop will consist of invited talks and technical presentations. Contributions are expected in all the areas of theoretical computer science, including the following: * Logical and algebraic foundations for computer science (logics for computer science, category theory, relation algebras, type theory, etc.), * Formal program construction (formal specification of sequential and concurrent programs; analysis, verification and transformation of programs, etc.), * Algorithms and data structures (sequential, parallel, distributed, on-line, probabilistic, etc.), * Computational complexity, * Automata theory, * Graph theory, * Symbolic and algebraic computation. The expected contributions will describe original results as well as undergoing research and development projects on theoretical computer science coming from academy and industry. Papers will be refereed by the International Program Committee, based on the following: * Papers reporting research / experimental results: these papers must present previously unpublished results and will be judged based on their originality, significance, relevance and clarity of presentation. Authors must submit an extended abstract of up to 4 pages containing enough information to allow the referees to determine the merits of their work. It is also allowed to submit the full paper of up to 12 pages including figures and references. * Research projects: aiming to fostering the cooperation among national and foreign researchers, short papers describing ongoing research will be considered. Papers in this category may report already published results. In that case, the authors must include the corresponding references. * Industrial / Commercial applications: also relevant are papers describing applications of theoretical results to real-life situations. Short papers describing results that are both of significance for industry and that make novel or defying applications of theoretical results are sought. INVITED SPEAKERS Thomas S. E. Maibaum (Imperial College, London, UK) Bernhard Moeller (Universitaet Augsburg, Germany) INSTRUCTIONS FOR AUTHORS: In order to facilitate the widest dissemination of the papers, authors are recommended the use of the English language. Nevertheless, papers in Spanish or Portuguese are also welcome. The deadline for submission of papers is May 3rd, 1999. Papers must be submitted electronically in PostScript format (ghostview-readable) to the e-mail address: wait99(a)sol.info.unlp.edu.ar Authors must send in a separate message in ASCII format the following: title of the paper, name and affiliation of all the authors, their e-mail addresses, phone and FAX numbers, an abstract of their contribution of at most ten lines, a list of keywords that best describe the paper, and also the category within which the paper is to be evaluated. Alternative ways for paper submission are possible and must be discussed with the workshop co-chairs. The format for camera-ready papers will be announced with the letter of acceptance. IMPORTANT DATES: Deadline for reception of papers....................May 3rd, 1999 Notification of acceptance..........................June 15th, 1999 Deadline for reception of camera-ready versions.....July 16th, 1999 WORKSHOP CO-CHAIRS: Prof. Gabriel Baum LIFIA Dto. de Informatica Universidad Nacional de La Plata Calle 50 y 115 1er piso. (1900) La Plata - Argentina Tel/Fax : +54-21-22-8252 e-mail: gbaum(a)sol.info.unlp.edu.ar Prof. Marcelo Frias Dpto. De Computacion -FCEyN- Universidad de Buenos Aires Pabellon I - Ciudad Universitaria 1428- Buenos Aires - ARGENTINA Tel/Fax : +54-1-783-0729 e-mail: mfrias(a)sol.info.unlp.edu.ar PROGRAM COMMITTEE: Gabriel Baum (Universidad Nacional de La Plata, Argentina) Javier Blanco (Universidad Nacional de Cordoba, Argentina) Luis FariÃ±as del Cerro (Universite Paul Sabatier, France) Esteban Feuerstein (Universidad Nacional de Buenos Aires and Universidad Nacional de General Sarmiento, Argentina) Marcelo Frias (Universidad Nacional de Buenos Aires, Argentina) Armando Haeberer (Pontificia Universidade Catolica de Rio de Janeiro, Brazil) Edward Hermann Haeusler (Pontificia Universidade Catolica de Rio de Janeiro, Brazil) Joos Heintz (Universidad Nacional de Buenos Aires, Argentina) Roger Maddux (Iowa State University, USA) Tom Maibaum (Imperial College, UK) Bernhard Moeller (Universitaet Augsburg, Germany) Gonzalo Navarro (Universidad de Chile, Chile) Alfredo Olivero (Universidad Nacional de Buenos Aires and Universidad Nacional de General Sarmiento, Argentina) Ruy de Queiroz (Universidade Federal de Pernambuco, Brazil) Alvaro Tasistro (Universidad de la Republica, Uruguay) Sergio Yovine (CNRS-VERIMAG, France) For more information send e-mail to: jaiio(a)sadio.edu.ar, write to: SADIO / WAIT'99 Uruguay 252 2D 1015 - Buenos Aires ARGENTINA TEL: +54-1-3715755/4763950 FAX: +54-1-3723950 or see http://www.uba.ar/wwws/sadio ___________________________________________ Gabriel Baum LIFIA Facultad de Ciencias Exactas Universidad Nacional de La Plata Calle 50 y 115 - 1er piso (1900) La Plata e-mail: gbaum(a)sol.info.unlp.edu.ar Tel/Fax: +54 21 228252 ___________________________________________

1 1

list outage
by Bob Rosebrugh 31 Mar '99

31 Mar '99

Note from moderator: Posts sent to the categories list in the past few days (roughly since March 26) will have bounced back to the sender. The cause was, ironically, a sendmail patch to scan for the "Melissa" virus/worm that corrupted the alias database for the majordomo software used by the list. If you sent a post recently and have not seen it please resend,things are working again. Sorry about any delays, and thanks to the Mount Allison network manager for immediate response when the problem was detected. regards, Bob Rosebrugh

1 0

CTCS '99 (Deadline 23 April 1999)
by Martin Hofmann 30 Mar '99

30 Mar '99

CATEGORY THEORY AND COMPUTER SCIENCE (CTCS'99) 10-12 SEPTEMBER 1999, EDINBURGH, SCOTLAND SECOND CALL FOR PAPERS SUBMISSION DEADLINE: 23 APRIL 1999 CHANGED SUBMISSION PROCEDURE (see below) CTCS '99 is the 8th conference on "Category Theory and Computer Science." The purpose of the conference series is the advancement of the foundations of computing using the tools of category theory. While the emphasis is upon applications of category theory, it is recognized that the area is highly interdisciplinary. Topics of interest - - ------------------ include but are not limited to category-theoretic aspects of the following: concurrent and distributed systems constructive mathematics declarative programming and term rewriting domain theory and topology linear logic models of computation program logics, data refinement, and specification programming language semantics type theory Previous meetings have been held in Guildford (Surrey), Edinburgh, Manchester, Paris, Amsterdam, Cambridge, and S. Margherita Ligure (Genova). Programme committee - - ------------------- J. Adamek TU Braunschweig (Germany) N. Benton Microsoft Research, Cambridge (UK) R. Blute U. Ottawa (Canada) T. Coquand Chalmers (Sweden) M. Escardo LFCS Edinburgh (UK) M. Hasegawa Kyoto Univ. (Japan) M. Hofmann (Chair) LFCS Edinburgh (UK) P. O'Hearn Queen Mary West (UK) D. Pavlovic Kestrel Institute (California) H. Reichel TU Dresden (Germany) G. Rosolini U. Genova (Italy) A. Scedrov U. Penn (Pennsylvania) Organising Committee - - -------------------- S. Abramsky LFCS Edinburgh (UK) P. Dybjer Chalmers U. (Sweden) E. Moggi U. Genova (Italy) A. Pitts U. Cambridge (UK) Submission procedure - - -------------------- E-mail your contribution as a PostScript file to the programme chair (ctcs99(a)dcs.ed.ac.uk) to be received by 23 April 1999. Alternatively, you can send 5 hardcopies by air mail. Authors with restricted copying facilities may also send a single hardcopy. Please make sure mail submissions arrive before the deadline (we'll definitely take submissions postmarked 7 April 1999 or earlier.). We would appreciate an informal notification of intention to submit 2 weeks prior to the deadline. Papers should allow the Programme Committee to assess the merits of the work: in particular references and comparisons with related work should be included. Submission of material already published or submitted to other Conferences with Proceedings is not allowed. There is no strict page limit; however authors are strongly encouraged to try not to exceed 20 A4 pages. Conference proceedings will appear in Electronic Notes in Theoretical Computer Science (http://www.elsevier.com/locate/entcs) Paper copies of the proceedings will be available to participants at the conference. Important dates - - --------------- 9 April 1999 Notification of intention to submit 23 April 1999 Submission deadline 4 June 1999 Notification of authors of accepted papers 30 July 1999 Deadline for final versions of accepted papers Address for paper submissions - - ----------------------------- Martin Hofmann Laboratory for Foundations of Computer Science Division of Informatics JCMB, King's Buildings Mayfield Road Edinburgh EH9 3JZ Scotland Local organization - - ------------------ Monika Lekuse Laboratory for Foundations of Computer Science Division of Informatics JCMB, King's Buildings Mayfield Road Edinburgh EH9 3JZ Scotland Conference e-address ctcs99(a)dcs.ed.ac.uk - - -------------------- Conference homepage http://www.dcs.ed.ac.uk/home/ctcs99 - - ------------------- Related event 2nd APPSEM workshop, 6-9 September 1999 - - ------------- http://www.md.chalmers.se/Cs/Research/Semantics/APPSEM/index.html - ------- End of forwarded message ------- ------- End of forwarded message -------

1 0

PhD Studentship at Edinburgh
by Gordon Plotkin 25 Mar '99

25 Mar '99

Division of Informatics University of Edinburgh Announcement of PhD Studentship in The Structure of Programming Languages: Syntax and Semantics A PhD student is sought for three years from October 1999 to work under the supervision of Prof. Gordon Plotkin on a UK EPSRC-funded project: ``The Structure of Programming Languages: Syntax and Semantics.'' The project aims at a general theory of the syntax and semantics of programming languages. The student will work on a categorical theory of structural operational semantics and its relation to denotational semantics. (See http://www.dcs.ed.ac.uk/home/dt/lics97.ps.) Example topics include: variations on GSOS for computational effects other than non-determinism; linguistic expressions of categorical operational semantics; and a theory of language translation incorporating both denotational and operational semantics. The studentship is for three years and pays for all fees and includes maintenance (living expenses) at the usual EPSRC rate. The studentship will be held at the Laboratory for Foundations of Computer Science (LFCS), Division of Informatics, University of Edinburgh. The LFCS provides an ideal environment for postgraduate research. The first six months of postgraduate training are supported by a unique postgraduate course on the theory of computation. In addition, there are regular short courses on advanced research topics, and a number of forums provide weekly research seminars. The LFCS is particularly strong in the area of semantics of programming languages. The PhD studentship is relevant to computer science or mathematics graduates who are interested in at least one topic from: theory of programming languages, operational semantics, category theory. For additional information contact Gordon Plotkin: gdp(a)dcs.ed.ac.uk http://www.dcs.ed.ac.uk/home/gdp/ For an application form write to Eleanor Kerse PhD Admissions, Department of Computer Science, University of Edinburgh, JCMB, King's Buildings, Edinburgh EH9 3JZ Scotland or use the HTML form available from http://www.dcs.ed.ac.uk/deptinfo/admissions/phd ----------------------------------------------------------------------------- Prof. Gordon Plotkin E-Mail: gdp(a)dcs.ed.ac.uk LFCS, University of Edinburgh Tel: +44 131 650 5158 JCMB, The King's Buildings Fax: 667 7209 Edinburgh EH9 3JZ, UK http://www.dcs.ed.ac.uk/home/gdp/

1 0

On reflexivity
by Tom KRANTZ 20 Mar '99

20 Mar '99

A 'philosophical' interpretation of oriented graphs might be out of the scope of the categories mailing list, it seems elucidating to me though.(It could have been for Heraclit and Parmenides.) I suggest to consider vertices as states and edges as transitions. A reflexive edge corresponds to a transition from a state to itself. Two notions of morphism of oriented graphs come seem natural: - A rigid embedding which preserves difference of states - A notion of morphism which may equalize different states. The meaning of equality of states needs precision then. Coherence semantics deals with a different notion of graph. This is clear to me and can also be deduced from a discussion between Thomas Ehrhard and his student Pierre to which I assisted. This bears an answer to the question of reflexivity I think. Sincerely, Tom

1 0

Ronnie Brown's type-dream
by Paul Taylor 20 Mar '99

20 Mar '99

Ronnie Brown asked, > This is written from the point of view of someone who would like to see a > computational system which is much nearer to real mathematics than the > current widely used systems (Maple, Mathematica, and various more > specialised systems, e.g. Singular). .... > So my question is: does all this general theory of types give a clear > indication as to what should be, not necessarily a final, but certainly a > convenient theory adequate for expressing a majority of present day maths? > > Let's make up a test case: one should be able to code reasonably > conveniently the type of a general groupoid acting on exterior algebras > over a commutative ring, and also of course the category of such objects. > A groupoid acting on exterior algebras with zero multiplication should be > coercible to a groupoid acting on graded modules. > > I would prefer the sytem to be so simple that it will allow tests for > consistency of new proposed types. Also it should be easy to understand, > since it would represent nicely current practice. > > Is this idea a mirage? No, I don't think it's a mirage, though [help me somebody I need a good pun here] the answer I have in mind may involve some altered states of perception. For the moment I want to steer clear of the "computational" question, as I haven't begun work on that, and would like to read his "current widely used systems" to refer to set theory, elementary toposes, Martin-Lof type theory and so on. That being said, I wonder whether the discussion and results in my "Abstract Stone Duality" paper (that I advertised on "categories" in the new year and which has since been revised) might appeal to Ronnie. It bases "set theory" on topology and not vice versa. It identifies categories of open discrete and compact Hausdorff spaces that are both pretoposes, and therefore suitable for doing algebra in, though the open discrete spaces are more appropriate for this as they admit free algebras. I do, as I said, have a computational model in mind, but am not yet in a position to say anything about it. Paul This paper, like most of what I talk about, is accessible from my Hypatia page http://hypatia.dcs.qmw.ac.uk/author/TaylorP

1 0

my groupoid model
by Paul Taylor 20 Mar '99

20 Mar '99

Francois Lamarche says: > I still think that if I started working again in this field, > the problem I would zero in would be to get rid of the permutation groups, This would be a great pity. Girard's coherence spaces (see "Proofs and Types"), ordinary relational algebra (in which Shroeder identified the par, writing +, for it, I think, in 1895) and my model with groupoids all illustrate a common theme in the workings of models of linear logic. In all of these structures, there are extremely natural ways of defining the structure on disjoint unions and cartesian products, and of turning the structure inside out or upside down. These turn out to be the additive, multiplicative and negative connectives in linear logic. There are less natural ways of defining the structure on powersets, finite powersets and other variations on this theme. These are the exponentials. It is important to note that there are several different exponential operations available to interpret ! and ? . Girard got function spaces out of such constructions (as did Francois, myself and numerous other people). What I hope to show soon is how to get higher order logic too. Paul

1 0

Polymorphic lambda-calculus
by Elaine Gouvea Pimentel 20 Mar '99

20 Mar '99

Hi! I'd like to know if there is any categorical model for polymorphic lambda-calculus. Thanks, Elaine.

3 2

more on monoidal structure of graphs
by Francois Lamarche 20 Mar '99

20 Mar '99

Since Michael's posting leapfrogged Marco's in the aether (at least from the viewpoint of our server) what I'll be saying may not appear in the right order threadwise to some. Marco Grandis wrote: > > Would it not be simpler to work with REFLEXIVE GRAPHS and their cartesian > closed structure? > In my opinion, reflexive graphs are more natural than graphs: The answer is no, because of the application in mind. We want to consider a graph as a constructive binary relation X(x,y), where an edge x-->y is a proof that (x,y) are related. We also want to build such things by induction, using universal properties. Reflexivity is often a desirable feature of the free structures you want to build, but you don't want it to come for free, since it creates redundancies and can mess up the induction principle associated with the structure. In certain situations you want reflexivity to be a consequence of the induction principle. > Remark 3. > [The sequel is relevant for homotopy; I do not know if it may be relevant > in CS, but I always had the impression that abstract homotopy should be of > use there, eg with respect to deformations of processes, in some sense.] > There are two connections I know about between homotopy and computer science. The first has to do with process algebras, and originates in Eric Goubault's thesis, I think. Philippe Gaucher just sent a paper annoucement on this server about this line of research. The second connection is something Thomas Streicher, Martin Hoffmann and I discuss whenever we meet, which is not often enough. In constructive type theory there is a gadget called the Martin-L"of intensional equality predicate, J(x,y). So this is a version of equality, where you have to name the proofs that x=y. It has very simple (but rather mysterious) introduction and elimination rules, which can be translated as a universal property in a kind of higher-order universal algebra, where arities can not only be seen as finite sets, but also as families of sets, and families of families of sets and so on. In particular, since everything is a type, you have a type/predicate of equality proofs between equality proofs, and so on. For example given proofs that x=y and y=z, you can construct a proof that x=z, and you can do this uniformly, getting a term/algorithm J(x,y)*J(y,z) --> J(x,z) (here the * means a fibered product over y). But you cannot show that this operation is itself associative, it is only associative at a higher order. Ah! some kind of multiple category is involved! But so far all attempts to use higher-order categories to describe those weird algebras have failed. It only works at level one: when you collapse all proofs of equality between proofs of equality you get that the predicate J(x,y) is a groupoid structure. But when you try to go to level 2 the ordinary 2- or bi- or lax- or whatever- categorical machinery fails. You realize that simplicial sets are a better paradigm/starting point, but we need simplicial sets with operations. BTW is anybody from G"oteborg reading this? > This is why I think that the basic 2-dimensional categorical setting for > abstract homotopy should only treat such "reduced horizontal composition": > arrows with cells, cells with arrows, but NOT cells with cells. > Formally, it is again a category enriched over reflexive graphs, BUT wrt > the following monoidal closed structure: > > X tensor Y: > - the subgraph of XxY whose arrows are pairs (a, b), where a or b > is an identity; > > [X, Y]: > - vertices: the graph morphisms; > - arrows: their transformations (without "diagonals"). > Hm... the geometrical motivations for not having full composition(s) here might well be related to the logical ones I mentioned briefly above. Francois

2 1

polymorphic lambda-calculus.
by Paul Taylor 19 Mar '99

19 Mar '99

Elaine Gouvea Pimentel would "like to know if there is any categorical model for polymorphic lambda-calculus". Oh dear. I can see that this one is going to haunt me for the rest of my life, besides provoking some "discussion" here. I wrote my thesis on this subject. Perhaps I will be personally rid of this albatross when my book comes out. Chapter VIII contains the definitive account of [my] notion of a "category with a class of display maps" (or, more briefly, display category). This is how I deal with dependent types at the algebraic level (superseding essentially algebraic theories encoded as categories with all finite limits). In my view, discussion of quantifiers (whether first order or over types) should be based on this, as is in fact done in Chapter IX. There are several different things that you might mean by "polymorphic lambda-calculus", and no doubt Bart Jacobs or Thomas Streicher will contribute an overview of the "Barendregt cube". [Robert Seely also did some work in this area before most of the other people.] One thing is that types are expressions involving type variables, with a universal quantifier over types. Girard calls this System F, and there is an introductory account in "Proofs and Types" - Girard's book that Yves Lafont and I translated. Numerous domain theoretic models of System F were found in the later 1980s, using both "Scott"-like "continuous" domains and "stable" domains which were introduced by Berry and popularised by Girard. ALL of the domain theoretic models, so far as I am aware, had THE SAME interpretation of type-dependency and the quantifier. I have seen this interpretation attributed to Girard, but I regarded it as "well known" when I was writing my thesis - before Girard's models - and my guess is that it is due to Gordon Plotkin, probably in the "Pisa notes". This interpretation of the dependency of the type T[x] on x:X, where X is in the first instance a domain (and in particular a poset, therefore a category) is most simply described as a functor T:X->Dom^adj where Dom^adj denotes the category whose objects are domains and whose morphisms are [left] adjoint pairs of continuous functions. Many authors took embeddings (monos with continuous right adjoints) instead, but the restriction is irrelevant. The functor T must also be continuous in the sense of taking directed joins to filtered colimits of left adjoints, which are also the cofiltered limits of the right adjoints. For the stable case, replace "continuous" by "stable", where a stable functor preserves pullbacks, and the unit and counit of the adjunctions have pullbacks for their naturality squares. This situation is so over-constrained that some pretty amazing things (that I discovered but never wrote up) happen. The universal quantifier is most concisely described as the category of sections of the fibration (Grothendieck construction) corresponding to the functor T above. That was for first order dependency over a particular domain X. For dependency over all domains (System F), replace X by Dom^adj. It doesn't matter whether this category happens to be one of your (poset) domains, so long as you only want System F. (At the time of my thesis I considered this to be cheating, and laboriously constructed a poset-domain that "covered" Dom^adj in a suitable sense. Thierry Coquand and his co-authors did not consider this to be cheating, and thereby beat me to finding a model of System F.) If Dom^adj really is a domain then you get a model of Coquand's Calculus of Constructions. Such a model of CoC was described by Martin Hyland and Andy Pitts in the Boulder proceedings in 1987. If I still had the inclination to work on such matters, I could give a simpler version of their model (replacing the lex categories by display categories). This was on the "to do" list throughout the writing of my book - I wanted to include this "simplified" version as a sequence of exercises - but it was always just over the horizon of what could be done with the tools available, given that the necessary domain-theoretic techniques had been debarred from the book from its conception. Another model, whose types are named by countable groupoids (or by the corresponding presheaf toposes of G-sets) is to be found in my paper "Quantitative Domains, Groupoids and Linear Logic" in the proceedings of the 1989 Manchester CTCS. When I was writing this paper I tried to get Francois Lamarche to read it, but he said he didn't know anything about / hated permutation representations. Nobody else, so far as I can gather, has ever read it, and now I can no longer follow the most difficult calculations. However, it is a very pretty model nevertheless. All of this was a bit of a Holy Grail. When you come to calculate the interpretations of types like Pi X. X -> (X->X) -> X, they turn out to be the most horrendous mess. The "coherence space" model in "Proofs and Types" may well be the only one in which you can give an explicit desciption of Pi X. X -> X -> X, and even that has four elements, where there are only two closed lambda terms. There are of course other ways of finding models of the polymorphic lambda calculus, such as using the "small complete category" in Hyland's effective topos, but I'll leave someone else to write about that. In conclusion, this particular dragon's den has already been explored, and the corpses are still there to prove it. Paul You can find this stuff on my page at Hypatia, http://hypatia.dcs.qmw.ac.uk/author/TaylorP and on the corresponding pages of the other people mentioned above.

2 1