October 2005 - Categories - categories.org.au

PhD position in Monadic Computational Logics
by Lutz Schroeder 17 Jan '06

17 Jan '06

A 3-year PhD-Position is available in the project "Monadic Computational Logics in HOL" at the University of Bremen. The project is concerned with the implementation and further development of monadic computational logics, including monadic Hoare logic and monadic dynamic logic as well as extensions covering exception handling, as introduced by Till Mossakowski and myself. More detailed information can be found at http://www.informatik.uni-bremen.de/~lschrode/research/projects/HOL-MDL_e.h… Applications or further enquiries may be e-mailed to my address below. -- Lutz -- ----------------------------------------------------------------------------- Lutz Schroeder Phone +49-421-218-4683 Dept. of Computer Science Fax +49-421-218-3054 University of Bremen lschrode(a)informatik.uni-bremen.de P.O.Box 330440, D-28334 Bremen http://www.informatik.uni-bremen.de/~lschrode -----------------------------------------------------------------------------

2 1

Generalizing bicategories
by George Janelidze 31 Oct '05

31 Oct '05

Dear All, In addition to all comments and references given to John Baez, I would like to mention MSc Thesis of my student Nelson Martins-Ferreira, and the paper N. Martins-Ferreira: "Weak categories in additive categories with kernels", Fields Institute Communications, Vol. 43, 2004, 387-410 (and its references). Nelson uses a notion of an internal weak category in a 2-category there (Page 391, Definition 6) and several related/more special notions to develop a convenient setting for 2-dimensional "abelianization". And I would like to use this opportunity to repeat few remarks on the story of abelianization of categorical structures, which I briefly made in my talk on CT1995 in Halifax: (i) It is well known (precise references to be found in various surveys of Ronnie Brown) for a long time that internal 2-categories in an additive category A with kernels can be identified with composable pairs (f,g) of morphisms in A with fg = 0, and that the same is true for n-categories, with n-sequences instead of pairs. Hence, whenever somebody comes up with, say, a new notion of a weak n-category, I would ask: what are the internal weak n-categories in YOUR sense in the category Ab of abelian groups? (Of course this question is "Yoneda invariant", and so there is no difference between considering the category Ab and considering an abstract additive category with kernels here) (ii) Why do we expect a simple answer to the question above? The point is, that most of higher categorical structures involve composition/coherence maps between pullbacks of split epimorphisms - and in the additive case, using kernels of those morphisms, one presents such pullbacks as direct sums and the composition/coherence maps as matrices. Therefore I expect an internal weak n-category in YOUR sense in the category of abelian groups to be nothing but an additive functor from a fixed finitely generated category X to Ab. The only question is: what is X? (iii) There are many examples showing that making comparisons between higher categorical structures might be highly nontrivial; so why not examining first what will happen to them in the simple additive/abelian world? Furthermore, and more generally, if T is a finite limit theory, then the free-forgetful adjunction between Sets and Ab "induces" an adjunction between Models(T) = Models(T,Sets) and Models(T,Ab), and the abelianization (=the left adjoint in that adjunction) Models(T) ---> Models(T,Ab) should help to study the category Models(T). Note that when T is the theory of groups, the abelianization functor becomes the usual one, and so it coincides with the first homology group functor (with coefficients in the additive group of integers). Answering the question from (i), one would certainly begin with bicategories, and, as far as I know, Nelson was the first who has described internal bicategories in additive categories with kernels, and I gave a talk on Nelson's work on Australian Category Seminar in March 2002 - before Nelson himself presented his more general results on the Meeting on Galois Theory, Hopf Algebras, and Semiabelian Categories at Field Institute (Toronto, September 2002). Now results: As shown by Nelson in the abovementioned paper (Section 5.2), an internal weak category in Mor(Ab) (=Cat(Ab)) (which is a special case of Nelson's more general result!) can be identified with a diagram in Ab consisting of morphisms d : A_1 ---> A_0, d' : B_1 ---> B_0, k : A_1 ---> B_1, k' : A_0 ---> B_0, l, r : A_0 ---> A_1, and h : B_0 ---> A_1 with k'd = d'k, kl = kr = 0 and kh = 0. It becomes (a) a bicategory, if B_1 = 0; (b) a double category if l = r = 0 and h = 0; (c) hence, a 2-category if B_1 = 0, l = r = 0 and h = 0. Nelson also examines what would happen without the coherence conditions, and then gets much more complicated formulas (See Proposition 6 in his paper). What Nelson has not done is what Tom Leinster calls "weakening in both directions". Another temptation is the (non-abelian) group case, hence generalizing crossed complexes. Let me also mention S. E. Crans: "Teisi in Ab", Homology, Homotopy and Applications 3, 2001, 87-100, although I do not know if anyone has considered a "double-" version of Crans' teisi. George Janelidze

1 0

abelian stuff
by Peter Freyd 30 Oct '05

30 Oct '05

At the recent Ottawa conference I repeated, in passing, something I've been saying for over 30 years: given a subcategory of an abelian category the finite bi-closure is, of course, obtainable by alternately adjoining limits and colimits countably often; remarkably enough, one need only do two cycles (assuming direct sums that's kernels, cokernels, kernels, cokernels). The proof is a consequence of of the construction of free abelian categories. Susan asked me later if I had ever actually worked out a direct proof. Nope. But it became apparent to me, thinking about what I had had to say about free abelian categories that I didn't know 30 years ago, that it shouldn't take two cycles, just one: In the abelian setting, adjoining finite limits commutes with adjoining finite colimits. (No -- for those old enough to remember -- this is not still 1969 and Ottawa is not Seattle.) There are some finicky points one must deal with when talking about images of functors (in the case at hand, functors such as those that assign kernels to maps), so let me just cut here to a critical little lemma that says, in effect, "a kernel of a map between cokernels is a cokernel of a map between kernels:" LEMMA: In an abelian category an exact diagram of the form (all vertical arrows are downwards): c B --> A --> F --> O b | a | | B'--> A'--> F'--> O c' may be enlarged to an exact diagram of the form: O --> K'--> A + B'+ B --> A + A' | | | O --> K ----> A + B'------> A' | c B --> A --> F --> O b | a | | B'--> A'--> F'--> O c' The exactness of K'--> K --> F --> F' says, precisely, that the kernel of F --> F' is the cokernel of K'--> K. The middle vertical K --> F is K --> A + B'--> A --> F where A + B'--> A is the projection map. (For present purposes a projection map is one given by a matrix in which each entry is 1 if such fits else 0.) The two top-right vertical maps are also projection maps. The two top-right horizontal maps are given (as luck would have it) by matrices in which each entry is 1 or a single letter (a,b,c,c') if such fits, else 0. It's not hard to verify this lemma in the category of abelian groups, which -- given the exact representation theorem -- suffices for all abelian categories. As if often the case, the proof of the dual of the lemma harder in the concrete case: CO-LEMMA: In an abelian category an exact diagram of the form (all vertical arrows are downwards): c' O --> K'--> A'--> B' | | a | b O --> K --> A --> B c may be enlarged to an exact diagram of the form: c' O --> K'--> A'--> B' | | a | b O --> K --> A --> B c | A'------> A + B'----> F --> O | | | A'+ A --> A + B'+ B --> F'--> O For the record, note that "a kernel of a map between kernels is a kernel," that is, the same initial exact diagram may be enlarged to a diagram:with exact rows and exact left column: O | O ---> K''--> A'--> A + B; | | | c' O ---> K'---> A'----> B' | | a | b O ---> K ---> A ----> B c The two upper-right verticals are projection maps and the upper right horizontal map is given by a matrix in which each entry is a single letter (a,c'). Also for the record: the finite bi-completion of an additive category is not abelian. Start with the additive closure of a single map f:A --> B. In the finite bi-completion the canonical map from Cok(Ker(f)) to Ker(Cok(f)) will not be an isomorphism. In the finite _abelian_ finite bi-completion, of course, it must be. (It is precisely this isomorphism, invoked at the end of the Lemma in the case f = K --> F, that delivers the commutativity of finite left and right completions.)

1 0

weak double categories?
by John Baez 29 Oct '05

29 Oct '05

Dear Categorists - If you weaken the notion of 2-category you get the notion of bicategory. Has anyone tried to correspondingly weaken the notion of double category, so that a bicategory is a special sort of "weak double category" in analogy to the ways in which a 2-category is a special sort of double category? Did anyone succeed? Best, jb

5 6

FM'06 Announcement and Call for Submissions
by events-admin＠fmeurope.org 29 Oct '05

29 Oct '05

FM'06: 14TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS 21 - 27 August 2006 McMaster University, Hamilton, Ontario, Canada http://fm06.mcmaster.ca/ ANNOUNCEMENT AND CALL FOR SUBMISSIONS FM'06 is the fourteenth in a series of symposia organized by Formal Methods Europe, http://www.fmeurope.org, an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. The symposia have been notably successful in bringing together innovators and practitioners in precise mathematical methods for software development, industrial users as well as researchers. Submissions are welcomed in the form of original papers on research and industrial experience, proposals for workshops and tutorials, entries for the exhibition of software tools and projects, and reports on ongoing doctoral work. FM'06 welcomes all aspects of formal methods research, both theoretical and practical. We are particularly interested in the experience of applying formal methods in practice. The broad topics of interest of this conference are: * Tools for formal methods: tool support and software engineering, environments for formal methods. * Theoretical foundations: specification and modelling, refining, static analysis, model-checking, verification, calculation, reusable domain theories. * Formal methods in practice: experience with introducing formal methods in industry, case studies. * Role of formal methods: formal methods in hardware and system design, method integration, development process. TECHNICAL PAPERS Full papers should be submitted via the web site. Papers will be evaluated by the Program Committee according to their originality, significance, soundness, quality of presentation and relevance with respect to the main issues of the symposium. Accepted papers will be published in the Symposium Proceedings, to appear in Springer's Lecture Notes in Computer Science series, http://www.springeronline.com/lncs . Submitted papers should have not been submitted elsewhere for publication, should be in Springer's format, (see Springer's web site), and should not exceed 16 pages including appendices. A prize for the best technical paper will be awarded at the symposium. INDUSTRIAL USAGE REPORTS One day will be dedicated to sharing the experience -- both positive and negative -- with using formal methods in industrial environments. The Industry Day is organized by ForTIA, the Formal Techniques Industry Association, http://www.fortia.org . This year's Industry Day investigates the use of formal methods in security and trust. Invited papers on organizational and technical issues will be presented. Inquiries should be directed to the Industry Day Chairs; see the web site for details. WORKSHOPS We welcome proposals for one-day or one-and-a-half-day workshops related to FM'06. In particular, but not exclusively, we encourage proposals for workshops on various application domains. Proposals should be directed to the Workshop Chair. TUTORIALS We are soliciting proposals for full-day or half-day tutorials. The tutorial contents can be selected from a wide range of topics that reflect the conference themes and provide clear utility to practitioners. Each proposal will be evaluated on importance, relevance, timeliness, audience appeal and past experience and qualification of the instructors. Proposals should be directed to the Tutorial Chair. POSTER AND TOOL EXHIBITION An exhibition of both research projects and commercial tools will accompany the technical symposium, with the opportunity of holding scheduled presentations of commercial tools. Proposals should be directed to the Poster and Tools Exhibition Chair. DOCTORAL SYMPOSIUM For the first time, FM'06 will feature a doctoral symposium. Students are invited to submit work in progress and to defend it in front of "friendly examiners". Participation for students who are accepted will be subsidized. Submissions should be directed to the Doctoral Symposium Chair. SUBMISSION DATES Technical Papers, Workshops, Tutorials: Friday, February 24, 2006 Posters and Tools, Doctoral Symposium: Friday, May 26, 2006 NOTIFICATION DATES Technical Papers: Friday, April 28, 2006 Workshops, Tutorials: Friday, March 10, 2006 Posters and Tools, Doctoral Symposium: Friday, June 9, 2006 ORGANIZATION General Chair: Emil Sekerinski (McMaster) Program Chairs: Jayadev Misra (U. Texas, Austin), Tobias Nipkow (TU Munich) Workshop Chair: Tom Maibaum (McMaster) Tutorial Chair: Jin Song Dong (NUS) Tools and Poster Exhibition Chair: Marsha Chechik (U. Toronto) Industry Day Chairs: Volkmar Lotz (SAP France), Asuman Suenbuel (SAP US) Doctoral Symposium Chair: Augusto Sampaio (U. Pernambuco) Sponsorship Chair: Juergen Dingel (Queens U.) PROGRAM COMMITTEE Jean-Raymond Abrial (ETH Zurich) Alex Aiken (Stanford U.) Keijiro Araki (Kyushu U.) Ralph Back (Abo Akademi) Gilles Barthe (INRIA) David Basin (ETH Zurich) Ed Brinksma (U. Twente) Michael Butler (U. Southampton) Rance Cleaveland (U. Stony Brook) Jorge Cuellar (Siemens) Werner Damm (U. Oldenburg) Frank de Boer (U. Utrecht) Javier Esparza (U. Stuttgart) Jose Fiadeiro (U. Leicester) Susanne Graf (VERIMAG) Ian Hayes (U. Queensland) Gerard Holzmann (JPL) Cliff Jones (U. Newcastle) Gary T. Leavens (Iowa State U.) Rustan Leino (Microsoft) Xavier Leroy (INRIA) Dominique Mery (LORIA) Carroll Morgan (UNSW) David Naumann (Stevens) E.-R. Olderog (U. Oldenburg) Paritosh Pandya (TIFR) Sriram Rajamani (Microsoft) John Rushby (SRI) Steve Schneider (U. Surrey) Vitaly Shmatikov (U. Texas, Austin) Bernhard Steffen (U. Dortmund) P.S. Thiagarajan (NUS) Axel van Lamsweerde (U. Louvain) Martin Wirsing (LMU Munich) Pierre Wolper (U. Liege) LOCAL ORGANIZATION Publicity: Wolfram Kahl, Alan Wassyng, Jeff Zucker Tools, Posters, Book Exhibition: Spencer Smith Social Events: Ridha Khedri Local Arrangements:: William Farmer, Mark Lawford Events Co-ordinator: Ryszard Janicki _______________________________________________ events mailing list events(a)fmeurope.org http://www.fmeurope.org/mailman/listinfo/events

1 0

Coalgebras Conference in Cairo
by mhebert 27 Oct '05

27 Oct '05

Dear all, This is to announce the Conference Algebras and Coalgebras, Tools for Geometry, Physics and Computer Science to be held in Cairo, Egypt March 25-30, 2006. Conference page: http://develop.aucegypt.edu/maths/index.html The aim of the conference is to gather mathematicians, mathematical physicists, and computer scientists working in areas closely related to the theory and applications of algebras and coalgebras. Besides exchanging information about the traditional applications of algebras to geometry, physics and computer science in this conference we want to highlight the usefulness of coalgebraic structures in these fields. They appear, for example, in quantum group theory, in symplectic geometry and quantum field theory, in non-commutative geometry, and in computer science. Main Speakers: Prof. Tomasz Brzezinski, University of Wales, Swansea, UK Prof. Heinz-Peter Gumm, University of Marburg, Germany Prof. Pavel Kolesnikov, Sobolev Institute, Novosibirsk, Russia Prof. Juergen Fuchs, Karlstad University, Sweden Prof. Dirk Kreimer, IHES, Paris, France Prof. Shahn Majid, Queen Mary University, London, UK Prof. Robert Wisbauer, University of Duesseldorf, Germany Prof. Farahat Ali, Al-Azhar University, Egypt Organizing Committee: Ismail A. Amin (Cairo) Tomasz Brzezinski (Swansea) Mohamed Fahmy (Cairo) Robert Wisbauer (Duesseldorf) Mohamed Yousif (Cairo and Ohio) Contact: algebra(a)aucegypt.edu

1 0

Journal "Logical Methods in CS"
by Logical Methods in CS 25 Oct '05

25 Oct '05

---------------------------------------------------------------------- year 1 of a new journal year 1 of a new journal year one of a new journal -------------------------EXCUSE MULTIPLE COPIES----------------------- Dear Colleague: We are writing to inform you about the progress of the open-access, online journal "Logical Methods in Computer Science," which has recently benefited from a freshly designed web site, see: http://www.lmcs-online.org In the first year of its existence, the journal received 75 submissions: 21 were accepted and 22 declined (the rest are still in the editorial process). The first issue is complete, and we anticipate that will be three in all by the end of the calendar year. Our eventual aim is to publish four issues per year. We also publish Special Issues: to date, three are in progress, devoted to selected papers from LICS 2004, CAV 2005 and LICS 2005. The average turn-around from submission to publication has been 7 months. This comprises a thorough refereeing and revision process: every submission is refereed in the normal way by two or more referees, who apply high standards of quality. We would encourage you to submit your best papers to Logical Methods in Computer Science, and to encourage your colleagues to do so too. There is a flier and a leaflet containing basic information about the new journal on the homepage; we would appreciate your posting and distributing them, or otherwise publicising the journal. We would also appreciate any suggestions you may have on how we may improve the journal. Yours Sincerely, Dana S. Scott (editor-in-chief) Gordon D. Plotkin and Moshe Y. Vardi (managing editors) Jiri Adamek (executive editor)

1 0

FM'06: CFP
by event＠mail.in.tu-clausthal.de 21 Oct '05

21 Oct '05

========================================================================= FM'06: 14TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS 21 - 27 August 2006 McMaster University, Hamilton, Ontario, Canada http://fm06.mcmaster.ca/ ANNOUNCEMENT AND CALL FOR SUBMISSIONS FM'06 is the fourteenth in a series of symposia organized by Formal Methods Europe, http://www.fmeurope.org, an independent association whose aim is to stimulate the use of, and research on, formal methods for software development. The symposia have been notably successful in bringing together innovators and practitioners in precise mathematical methods for software development, industrial users as well as researchers. Submissions are welcomed in the form of original papers on research and industrial experience, proposals for workshops and tutorials, entries for the exhibition of software tools and projects, and reports on ongoing doctoral work. FM'06 welcomes all aspects of formal methods research, both theoretical and practical. We are particularly interested in the experience of applying formal methods in practice. The broad topics of interest of this conference are: * Tools for formal methods: tool support and software engineering, environments for formal methods. * Theoretical foundations: specification and modelling, refining, static analysis, model-checking, verification, calculation, reusable domain theories. * Formal methods in practice: experience with introducing formal methods in industry, case studies. * Role of formal methods: formal methods in hardware and system design, method integration, development process. TECHNICAL PAPERS Full papers should be submitted via the web site. Papers will be evaluated by the Program Committee according to their originality, significance, soundness, quality of presentation and relevance with respect to the main issues of the symposium. Accepted papers will be published in the Symposium Proceedings, to appear in Springer's Lecture Notes in Computer Science series, http://www.springeronline.com/lncs . Submitted papers should have not been submitted elsewhere for publication, should be in Springer's format, (see Springer's web site), and should not exceed 16 pages including appendices. A prize for the best technical paper will be awarded at the symposium. INDUSTRIAL USAGE REPORTS One day will be dedicated to sharing the experience -- both positive and negative -- with using formal methods in industrial environments. The Industry Day is organized by ForTIA, the Formal Techniques Industry Association, http://www.fortia.org . This year's Industry Day investigates the use of formal methods in security and trust. Invited papers on organizational and technical issues will be presented. Inquiries should be directed to the Industry Day Chairs; see the web site for details. WORKSHOPS We welcome proposals for one-day or one-and-a-half-day workshops related to FM'06. In particular, but not exclusively, we encourage proposals for workshops on various application domains. Proposals should be directed to the Workshop Chair. TUTORIALS We are soliciting proposals for full-day or half-day tutorials. The tutorial contents can be selected from a wide range of topics that reflect the conference themes and provide clear utility to practitioners. Each proposal will be evaluated on importance, relevance, timeliness, audience appeal and past experience and qualification of the instructors. Proposals should be directed to the Tutorial Chair. POSTER AND TOOL EXHIBITION An exhibition of both research projects and commercial tools will accompany the technical symposium, with the opportunity of holding scheduled presentations of commercial tools. Proposals should be directed to the Poster and Tools Exhibition Chair. DOCTORAL SYMPOSIUM For the first time, FM'06 will feature a doctoral symposium. Students are invited to submit work in progress and to defend it in front of "friendly examiners". Participation for students who are accepted will be subsidized. Submissions should be directed to the Doctoral Symposium Chair. SUBMISSION DATES Technical Papers, Workshops, Tutorials: Friday, February 24, 2006 Posters and Tools, Doctoral Symposium: Friday, May 26, 2006 NOTIFICATION DATES Technical Papers: Friday, April 28, 2006 Workshops, Tutorials: Friday, March 10, 2006 Posters and Tools, Doctoral Symposium: Friday, June 9, 2006 ORGANIZATION General Chair: Emil Sekerinski (McMaster) Program Chairs: Jayadev Misra (U. Texas, Austin), Tobias Nipkow (TU Munich) Workshop Chair: Tom Maibaum (McMaster) Tutorial Chair: Jin Song Dong (NUS) Tools and Poster Exhibition Chair: Marsha Chechik (U. Toronto) Industry Day Chairs: Volkmar Lotz (SAP France), Asuman Suenbuel (SAP US) Doctoral Symposium Chair: Augusto Sampaio (U. Pernambuco) Sponsorship Chair: Juergen Dingel (Queens U.) PROGRAM COMMITTEE Jean-Raymond Abrial (ETH Zurich) Alex Aiken (Stanford U.) Keijiro Araki (Kyushu U.) Ralph Back (Abo Akademi) Gilles Barthe (INRIA) David Basin (ETH Zurich) Ed Brinksma (U. Twente) Michael Butler (U. Southampton) Rance Cleaveland (U. Stony Brook) Jorge Cuellar (Siemens) Werner Damm (U. Oldenburg) Frank de Boer (U. Utrecht) Javier Esparza (U. Stuttgart) Jose Fiadeiro (U. Leicester) Susanne Graf (VERIMAG) Ian Hayes (U. Queensland) Gerard Holzmann (JPL) Cliff Jones (U. Newcastle) Gary T. Leavens (Iowa State U.) Rustan Leino (Microsoft) Xavier Leroy (INRIA) Dominique Mery (LORIA) Carroll Morgan (UNSW) David Naumann (Stevens) E.-R. Olderog (U. Oldenburg) Paritosh Pandya (TIFR) Sriram Rajamani (Microsoft) John Rushby (SRI) Steve Schneider (U. Surrey) Vitaly Shmatikov (U. Texas, Austin) Bernhard Steffen (U. Dortmund) P.S. Thiagarajan (NUS) Axel van Lamsweerde (U. Louvain) Martin Wirsing (LMU Munich) Pierre Wolper (U. Liege) LOCAL ORGANIZATION Publicity: Wolfram Kahl, Alan Wassyng, Jeff Zucker Tools, Posters, Book Exhibition: Spencer Smith Social Events: Ridha Khedri Local Arrangements:: William Farmer, Mark Lawford Events Co-ordinator: Ryszard Janicki ------------------------------------------------------------------------ This e-mail was delivered to you by event(a)in.tu-clausthal.de, what is a moderated list runned by Computational Intelligence Group of Clausthal University of Technology, Germany. All event announcements sent through this list are also listed in our conference planner at http://cig.in.tu-clausthal.de/index.php?id=planner. In the case of any requests, questions, or comments, do not hesitate and contact event-owner(a)in.tu-clausthal.de ASAP. ****************************************************** * CIG does not take any responsibility for validity * * of content of messages sent through this list. * ****************************************************** Computational Intelligence Group Department of Computer Science Clausthal University of Technology Germany http://cig.in.tu-clausthal.de/

1 0

Ottawa weather
by Peter Freyd 21 Oct '05

21 Oct '05

Friday Scattered Clouds. High: 48F / 9C Wind WNW 4 mph / 7 km/h Friday Night Scattered Clouds. Low: 30F / -1C Wind North 4 mph / 7 km/h Saturday Scattered Clouds. High: 51F / 11C Wind NE 6 mph / 10 km/h Saturday Night Scattered Clouds. Low: 32F / 0C Wind NE 8 mph / 14 km/h Sunday Scattered Clouds. High: 48F / 9C Wind NE 15 mph / 25 km/h Sunday Night Rain. Low: 37F / 3C Wind ENE 15 mph / 25 km/h Monday Overcast. High: 41F / 5C Wind ENE 13 mph / 21 km/h

1 0

Research position in Coalgebras and Formal Verification at Southampton
by Corina Cirstea 19 Oct '05

19 Oct '05

*Research position in Coalgebras and Formal Verification* School of Electronics and Computer Science University of Southampton Declarative Systems and Software Engineering Group http://www.dsse.ecs.soton.ac.uk Closing date: 31 October 2005 Applications are invited for a Research Fellow in the Declarative=20 Systems and Software Engineering Group, in the School of Electronics and=20 Computer Science. The School is the largest of its kind in the UK, and=20 has internationally acknowledged research excellence in Electronics and=20 Computer Science (RAE 2001 Grade 5*/5*). The successful applicant will work on the EPSRC-funded research project=20 "Towards a Modular Approach to Model-Based Verification: logical,=20 semantical and algorithmic support". The project aims to develop modular=20 model-based verification techniques for state-based dynamical systems,=20 by using the mathematical theory of coalgebras as a unifying framework. Applicants should have (or be nearing the completion of) a PhD in=20 Computer Science or a related subject, and have a proven research record=20 in theoretical computer science/formal methods. Experience in one or=20 more of the following areas: logic, universal coalgebra, category=20 theory, formal specification, model checking is desirable. The salary=20 will be in the range =A322,774 - =A328,009. The post is available for two= =20 years, from 01/01/2006. Informal enquiries should be addressed to Dr Corina C=EErstea, Tel: +44=20 (0)23 8059 3625, e-mail: cc2(a)ecs.soton.ac.uk. An application form and further particulars may be obtained from the=20 Human Resources Department (R), University of Southampton, Highfield,=20 Southampton, SO17 1BJ, Tel: 023 8059 2750, e-mail: recruit(a)soton.ac.uk=20 or minicom: 023 8059 5595, alternatively visit our website at=20 www.jobs.soton.ac.uk. Closing date for applications 31/10/2005. Please=20 quote reference number 05R0160C. ----------------------------------------------------------------------- Dr Corina Cirstea Electronics and Computer Science University of Southampton Southampton, SO17 1BJ United Kingdom Tel: +44 (0)23 8059 3625 -----------------------------------------------------------------------

1 0