June 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

Job: Lectureship
by Alexander Kurz 05 Oct '05

05 Oct '05

Apologies for multiple postings ------------------------------- Please distribute to potential candidates ----------------------------------------- The University of Leicester seeks to appoint two Lecturers (tenure track) who can contribute to existing research in the foundations and applications of algebraic structures and methods in general, and the emerging area of service-oriented computing in particular ... (see the URL below for more) In particular, we are looking for one person who can complement our strengths in theoretical research which is currently represented by Roy Crole, Alexander Kurz, Vincent Schmitt and Fer-Jan de Vries. The official announcement should be available soon at http://www.le.ac.uk/personnel/jobs/a&r.html Closing date is (probably, see URL above) 5 July 2005. If you have any informal enquires please contact one of us. 15-Jun-2005 19:59:14 -0300,7560;000000000000-00000012

2 2

postdoc position: semantics of nondeterminism
by Paul B Levy 29 Jun '05

29 Jun '05

Dear colleagues, A postdoctoral Research Fellowship lasting 32 months is available in the School of Computer Science, University of Birmingham, starting any time from 1 July 2005 to 1 January 2006, working in the semantics of nondeterminism. The application deadline is 22 July 2005. Application details can be found at http://www.punit.bham.ac.uk/vacancies/furtherParticulars.htm?refNo=36914 The School of Computer Science is a major centre for research and teaching in Computer Science and has around 130 researchers, with a lively and friendly atmosphere that encourages research straddling different themes. The vibrant Theory Group spans the spectrum from programming languages to mathematical foundations. Its research includes game, domain, effect, pointer and categorical semantics, topology, logic, model-checking and much else besides. The School has recently hosted the Midlands Graduate School (April 2005) and Mathematical Foundations in Programming Semantics (May 2005). Semantics of nondeterminism --------------------------- To reason about a computer system, it is often necessary to idealize it as nondeterministic, i.e. possessing a range of possible behaviours. The factors that determine its actual behaviour are too low-level and complex to consider explicitly. But this apparently simple idea has ramifications for the theory of programming language semantics that are not well understood. They centre on the question: what does it mean for 2 programs to be equivalent? Previous research has used mathematical structures known from the theory of deterministic programs. But these have limited applicability to nondeterministic programs, and lead to somewhat awkward notions of equivalence. This research will proceed in the opposite direction: begin with certain computationally natural notions of equivalence, and investigate what structures they lead to. Aspects of this research may include: - formulating game semantics that build on existing game models and on existing ways of reasoning about nondeterminism (e.g. Howe's method for congruence of bisimilarity) - studying higher-order languages with nondeterminism, building on existing calculi (e.g. call-by-push-value, Affine HOPLA, etc.), and diverse semantics of such languages - analyzing definability of functions at low order. There is plenty of scope for developing these themes in different directions. Applicants must hold a PhD (or expect to attain one before taking up the appointment). A research background in any or all of the following would be useful: * category theory * semantics of programming languages * game semantics * semantics of concurrency Please do not hesitate to contact me with any queries. Regards Paul -- Paul Blain Levy email: pbl(a)cs.bham.ac.uk School of Computer Science, University of Birmingham Birmingham B15 2TT, U.K. tel: +44 121-414-4792 http://www.cs.bham.ac.uk/~pbl 30-Jun-2005 12:03:57 -0300,1786;000000000000-00000020

1 0

Fields Institute program announcement
by Rick Jardine 29 Jun '05

29 Jun '05

Announcement: Thematic Program on Geometric Applications of Homotopy Theory Fields Institute Toronto, Canada January-June 2007 This research program will develop new applications of homotopy theory in algebraic geometry, number theory and mathematical physics, and will include subprograms on the homotopy theory of schemes, stacks in geometry and topology, and higher categories and their applications. The overall program organizers are: Rick Jardine (Western Ontario), Lead Organizer, jardine(a)uwo.ca Gunnar Carlsson (Stanford), gunnar(a)math.stanford.edu Dan Christensen (Western Ontario), jdc(a)uwo.ca Each subprogram will be two months in duration, and will incorporate graduate courses and five-day workshops. The subprograms, their organizers, and dates of the workshops are the following: 1) Higher categories and their applications (January-February) J. Baez (Univ. of California, Riverside) E. Cheng (Chicago) P. May (Chicago) Workshop: January 9-13, 2007 2) Homotopy theory of schemes (March-April) E. Friedlander (Northwestern) M. Karoubi (Paris VII) M. Kolster (McMaster) Workshop: March 26-30, 2007 3) Stacks in geometry and topology (May-June) K. Behrend (British Columbia) P. Goerss (Northwestern) B. Toen (Paul Sabatier, Toulouse) Workshop: May 14-18, 2007 Funding will be available for junior researchers and graduate students; an on-line application will be available in 2006. The conference website is http://www.fields.toronto.edu/programs/scientific/06-07/homotopy/ Further information about the program will appear on this website, as it becomes available. 30-Jun-2005 09:15:50 -0300,3659;000000000000-0000001f

1 0

research vacancies in Amsterdam (VU, CWI) and Utrecht
by Roel de Vrijer 29 Jun '05

29 Jun '05

======================================================================= Vrije Universiteit Amsterdam ++ CWI Amsterdam ++ Utrecht University Three research positions in the NWO-sponsored project INFINITY: Infinite Objects, computation, modeling and reasoning ======================================================================= We are seeking three researchers at the level of Postdoc or Asssociate Professor (UD) for a period of two to three years. Candidates should have - Good knowledge of at least one and preferably more of the following fields: Term rewriting, Graph rewriting, Lambda calculus, Proof theory, Co-algebra, Co-induction, Logic and Automated Reasoning, Type theory - For a postdoc position: a (nearly) finished PhD in computer science, mathematics or logic - For a UD position: several additional years of research experience Starting date of the project is September 1st, 2005. Description of the project -------------------------- We consider infinite objects, such as streams, infinite trees, infinite terms and term graphs, both first order and higher order (with binders as in lambda calculus) or infinite communicating processes. Often these exhibit a regular or cyclic nature, but we are also interested in general infinite objects. A paradigm example is the coalgebra of infinite bitstreams. Several operators can be defined on these objects, such as the operator zip that zips two streams alternatingly into one. Defining ones = 1 : one zeros = 0 : zeros alt = 0 : 1 : alt we have equations such as zip(zeros, ones) = alt The equations holding in this coalgebra between these objects and their operators can be proved in three different ways: by coalgebraic techniques, by proof theory, and by infinitary term rewriting. These three methods have been developed up to now in relative isolation. This project investigates the relations between these approaches and aims to design methods such as new proof systems to deal with the infinite objects and their equations. Issues are well-definedness criteria, completeness of the methods, decidability and implementation. Thus the project combines for infinite objects the activities of computing, modeling, and reasoning. For detailed information see the full project proposal. It will be sent to you on request (email to rdv(a)cs.vu.nl, please mention "INFINITY" in the subject). The positions ------------- The project is headed by Prof. Dr. J.W. Klop and is a collaboration between the following Dutch research groups: - Vrije Universiteit Amsterdam, section "Theoretical Computer Science" contact: Dr. R.C. de Vrijer, rdv(a)cs.vu.nl, phone: +31 (0)20 5987770 - CWI Amsterdam, the group "Coordination languages" contact: Prof. Dr. J.J.M.M. Rutten, jan.rutten(a)cwi.nl - Utrecht University, the group "Theoretical Philosophy" contact: Dr. V. van Oostrom, Vincent.vanOostrom(a)phil.uu.nl The research will be embedded in the broader framework of the themes of the three participating research groups: formal methods, logic, term and graph rewriting, lambda calculus, coalgebraic methods, process algebra. At each institution there is one position available. Roughly the focus of the three positions varies as follows, more details to be found in the full proposal. - Vrije Universiteit: Proof theory, Infinitary term rewriting - CWI: Co-algebra, theory and applications - Utrecht University: Infinitary term rewriting and implementation using graph rewriting Applications ------------ The full project proposal will be sent to you on request (rdv(a)cs.vu.nl) Further enquiries can be made with the contact persons. You are invited to send your application by email to the contact person of the institution for which you want to apply. Deadline for applications is July 17, 2005. In case you learn of this job opportunity later than that date you may send an email to enquire whether it still makes sense to apply. Your application should consist of: - a cover letter - a curriculum vitae (including detailed information regarding your academic degrees, title and subject of your PhD-thesis, publications) - the names and addresses of two references If you are interested in more than one of the offered positions you should clearly indicate so and give your motivation. It is not necessary to write separate letters. Please include "INFINITY" in the subject of all your emails. 29-Jun-2005 13:02:09 -0300,1968;000000000001-0000001d

1 0

Preliminary Announcement: CT06
by Robert J. MacG. Dawson 28 Jun '05

28 Jun '05

The members of the CT06 Organizing Committee hereby announce our intent to hold an international conference in category theory at White Point Beach Resort, from June 25 through July 1, 2006. White Point Beach Resort ( http://www.whitepoint.com/ ) is a seaside resort in Nova Scotia, about 100 minutes' drive from Halifax. There will be a choice of accommodation, both in comfortable finished cabins and in "hotel-style" rooms. Prices, including all meals, accommodation, and the use of conference facilities, will be in line with many other conferences. The facilities are large, and it is not anticipated that we will need to limit registration. The management has told us that we will be the only group using the conference facilities, sharing the resort as a whole with only a few vacationers. We anticipate an active research-oriented conference, in something of an "Oberwolfach style", with more opportunities for informal discussion and collaboration in the evenings than might be the case in an urban setting. There will also be many opportunities for recreational activities. We will announce further details soon. -Robert Dawson Dorette Pronk Richard Wood 29-Jun-2005 13:02:09 -0300,2450;000000000001-0000001e

1 0

Preprint : Inverting weak dihomotopy equivalence using homotopy continuous flow
by Philippe Gaucher 27 Jun '05

27 Jun '05

Dear All, Here is a new preprint. Sincerely yours. Title: Inverting weak dihomotopy equivalence using homotopy continuous flow Author: Philippe Gaucher Abstract: A flow is homotopy continuous if it is indefinitely divisible up to S-homotopy. The full subcategory of cofibrant homotopy continuous flows has nice features. Not only it is big enough to contain all dihomotopy types, but also a morphism between them is a weak dihomotopy equivalence if and only if it is invertible up to dihomotopy. Thus, the category of cofibrant homotopy continuous flows provides an implementation of Whitehead's theorem for the full dihomotopy relation, and not only for S-homotopy as in previous works of the author. This fact is not the consequence of the existence of a model structure on the category of flows because it is known that there does not exist any model structure on it whose weak equivalences are exactly the weak dihomotopy equivalences. This fact is an application of a general result of localization of a model category with respect to a weak factorization system. Comments: 22 pages, LaTeX2e Url: ArXiv or http://www.pps.jussieu.fr/~gaucher/ 29-Jun-2005 13:02:09 -0300,5223;000000000000-0000001c

1 0

Saunders on Hausdorff axiom
by Colin McLarty 24 Jun '05

24 Jun '05

It seems to me that somewhere Saunders wrote about taking an oral exam from Hermann Weyl where Weyl asked him what is a Hausdorff space, and Saunders could not think of it. But I cannot recall where I read that (or heard it?). Can anyone tell me? thanks, Colin 25-Jun-2005 11:24:05 -0300,1811;000000000000-0000001a

2 1

Preprint: Lax 2-categories and directed homotopy
by Marco Grandis 21 Jun '05

21 Jun '05

The following preprint is available: M. Grandis, Lax 2-categories and directed homotopy, Dip. Mat. Univ. Genova, Preprint 530 (2005), 18 p. Abstract. Directed Algebraic Topology is a recent field, where a 'directed space' X, e.g. an ordered topological space, has directed paths (which are generally not reversible) and a *fundamental category*, replacing the fundamental groupoid of the classical case. In dimension 2, the directed 2-dimensional paths of X naturally produce a fundamental *lax 2-category*. This is an extension of a bicategory where comparison cells are not assumed to be invertible, and some choice for their direction is needed. Our geometric guideline gives a choice which is different from the ones previously considered by Burroni, Borceux, Leinster. Available in pdf at: http://www.dima.unige.it/~grandis/LCat.pdf Marco Grandis Dipartimento di Matematica Universita` di Genova via Dodecaneso 35 16146 GENOVA, Italy e-mail: grandis(a)dima.unige.it tel: +39.010.353 6805 fax: +39.010.353 6752 http://www.dima.unige.it/~grandis/ 24-Jun-2005 07:20:14 -0300,1223;000000000000-00000019

1 0

PhD studentship, Probabilistic Model Checking with PRISM
by Marta Kwiatkowska 20 Jun '05

20 Jun '05

[Please forward to anyone interested. Apologies for multiple mailing.] ========================================================================= School of Computer Science, University of Birmingham Ph.D. Studentship in Probabilistic Model Checking ========================================================================= One PhD studentship is available in the School of Computer Science at the University of Birmingham to work on probabilistic model checking under the supervision of Professor Marta Kwiatkowska. Probabilistic model checking is an automatic verification method that can establish whether a given specification holds for a probabilistic system. For example, for the randomised Bluetooth protocol one might obtain quantitative answers to the expected time to device discovery and the probability of delivery by a deadline. PRISM (http://www.cs.bham.ac.uk/~dxp/prism/) the leading and widely used probabilistic model checker developed at the University of Birmingham under Kwiatkowska's leadership, is an open source tool that has been used to model and analyse over 30 real-world protocols, with flaws discovered in six of those. PRISM is a symbolic model checker, and it combines numerical solution techniques, simulation-based methods (for approximate analysis) and parallelization. This project is to contribute to the implementation of probabilistic model checking techniques within PRISM. Possible topics include an extension of probabilistic model checking to real source code, statistical model checking, efficient algorithms and data structures, probabilistic real-time verification and online analysis methods. More detail about this project is available at http://www.cs.bham.ac.uk/~mzk/research_probmc_stud.html Applicants are encouraged to contact Marta Kwiatkowska directly (email: mzk(a)cs.bham.ac.uk) and refer to her group's work on probabilistic modelling and verification (http://www.cs.bham.ac.uk/research/systems/probabilistic/) The studentship is available for UK and European applicants who want to work full time on their research degree and lasts for up to three years. Candidates should have, or be predicted to gain, a very good degree in computer science, mathematics or a relevant scientific discipline. Informal inquiries are welcome, preferably via e-mail. Information about admission for PhD in Computer Science at the University of Birmingham is available at http://www.cs.bham.ac.uk/study/postgraduate-research/. Applications can be made until 10th July 2005. Professor Marta Kwiatkowska, School of Computer Science, University of Birmingham, Edgbaston, Birmingham B15 2TT. E-mail: mzk(a)cs.bham.ac.uk URL: http://www.cs.bham.ac.uk/~mzk Tel: +44 121 4147264 Fax: +44 121 4144281 21-Jun-2005 14:05:02 -0300,1768;000000000001-00000018

1 0