February 2008 - Categories - categories.org.au

FM'08 -- CALL FOR PARTICIPATION
by events-admin＠fmeurope.org 23 Feb '08

23 Feb '08

*** Apologies if you receive multiple copies. *** FM'08: 15TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS May 26 - 30, 2008 Åbo Akademi University Turku, Finland CALL FOR PARTICIPATION http://www.fm2008.abo.fi/ It is our pleasure to invite you to FM'08, the premier international forum for practitioners and researchers applying mathematical methods to the design of highly reliable computer systems. FM'08 is the fifteenth 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. A program of five invited talks and 23 outstanding research papers provides the opportunity to learn about the newest developments in the theory and application of formal methods. The program covers a wide range of topics, including real-time and concurrency, design, verification, communication, runtime monitoring and analysis, constraint analysis, programming language analysis, formal methods practice, and grand challenge problems. As in the previous years, an Industry Day is dedicated for practitioners to share their experiences with industrial applications. This year's Industry Day investigates telecommunications and embedded systems, being supported by NOKIA. Speakers from five major industries will address this year's theme, together with the Johnson Professor Arvind from MIT. Tutorials are a central part of this years FM symposium, as an effective way of disseminating emerging application areas, tools, and techniques. This year we have seven tutorials, given by renowned experts in their fields. The five co-located workshops address issues of specific formal techniques as well as novel computational models and grand challenges. The following list of tutorials and workshops are available: Tutorials · Computational Systems Biology · Teaching formal methods to students in high school and introductory university courses · Event-B and the Rodin Platform · Why formal verification remains on the fringes of commercial development · Formal Methods and Signal Processing · Runtime Model Checking of Multithreaded C Programs using Automated Instrumentation Dynamic Partial Order Reduction and Distributed Checking · Formal modelling and analysis of real-time systems using UPPAAL Workshops · Formal aspects of virtual organisations · Overture/VDM++ · Refinement workshop · Pilot Projects for the Grand Challenge in Verified Software · Computational Models for Cell Processes A Doctoral Symposium on all aspects of formal methods research is also part of FM08, giving young researchers the opportunity to have their ideas critically, but constructively examined by the community. A Poster and Tool Exhibition of both research projects and commercial tools allows researchers to engage in a dialogue with potential users in early phases of their work. The submission date for the both the Doctoral Symposium and the Poster and Tool Exhibition is March 7. Registration to all types of events will open during week 8, with the possibility of early registration until March 25. Important dates for submitting papers to the workshops should be identified via the own homepages of these events, reachable from above or from the FM08 website. Generally, workshop papers should be submitted in March. The list of the accepted papers to the technical symposium and the preliminary schedule of FM08 can already be retrieved via our website. We hope you will enjoy a rewarding symposium program! Kaisa Sere, General Chair Jorge Cuellar, Tom Maibaum, Program Chairs _______________________________________________ events mailing list events(a)fmeurope.org http://www.fmeurope.org/mailman/listinfo/events

1 0

MFPS Final Call for Papers
by Michael Mislove 23 Feb '08

23 Feb '08

Dear Colleagues, This is the Final Call for Papers for MFPS 24. Details about the meeting are given below. Submissions should be made to EasyChair at the link http://www.easychair.org/conferences/?conf=mfps24 The deadline for submissions of titles and brief abstracts is Friday, March 7, and the deadline for full submissions is the following Friday, March 14. Thanks, and best regards, Mike Mislove =============================================== Professor Michael Mislove Phone: +1 504 862-3441 Department of Mathematics FAX: +1 504 865-5063 Tulane University URL: http://www.math.tulane.edu/~mwm New Orleans, LA 70118 USA =============================================== CALL FOR PAPERS MFPS XXIV http://www.math.tulane.edu/~mfps/mfps24.htm Twenty-fourth Conference on the Mathematical Foundations of Programming Semantics University of Pennsylvania Philadelphia, PA USA May 22 - 25, 2008 Partially Supported by US Office of Naval Research The MFPS conferences are devoted to those areas of mathematics, logic, and computer science which are related to models of computation, in general, and to the semantics of programming languages, in particular. The series has particularly stressed providing a forum where researchers in mathematics and computer science can meet and exchange ideas about problems of common interest. As the series also strives to maintain breadth in its scope, the conference strongly encourages participation by researchers in neighboring areas. TOPICS include, but are not limited to, the following: biocomputation; categorical models; concurrent and distributed computation; constructive mathematics; domain theory; formal languages; formal methods; game semantics; lambda calculus; logic; non-classical computation; probabilistic systems; process calculi; program analysis; programming-language theory; quantum computation; rewriting theory; security; specifications; topological models; type systems; type theory. The Twenty-fourth Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIV) will take place on the campus of University of Pennsylvania, Philadelphia, PA USA from Thursday, May 22 through Sunday, May 25, 2008. The Organising Committee for MFPS consists of Stephen Brookes (CMU), Achim Jung (Birmingham), Catherine Meadows (NRL), Michael Mislove (Tulane), and Prakash Panangaden (McGill). The local arrangements for MFPS XXIV are being overseen by Andre Scedrov (Penn). The INVITED SPEAKERS for MFPS XXIV are Samson Abramsky, Oxford Luca Cardelli, Microsoft Research, Cambridge Dusko Pavlovic, Kestrel Institute Benjamin Pierce, Penn Phil Scott, Ottawa James Worrell, Oxford In addition, there will be four special sessions: - A session honoring Phil Scott on the occasion of his 60th birthday year, which is being organized by Rick Blute (Ottawa) and Andre Scedrov (Penn). - A session on Systems Biology will be held in conjunction with Luca Cardelli's plenaary talk. It is being organized by Jean Krivine (LIX). - A third session will be devoted to Type Theory. It is being organized by Benjamin Pierce and by Robert Harper (CMU) will be held in conjunction with Benjamin Pierce's plenary talk. - The fourth special session will be on Security, and will be organized by Catherine Meadows (NRL) in conjunction with Dusko Pavlovic's plenary talk. Further, there will be a TUTORIAL DAY on May 21. The topic will be Category Theory and Its Applications to Theoretical Computer Science. It is being organized by Phil Scott (Ottawa); the speakers will be announced at a later date. This event will be free to all those who are interested in attending. The remainder of the program will consist of papers selected by the following PROGRAM COMMITTEE Andrej Bauer (Ljubljana), CHAIR Ulrich Berger (Swansea) Lars Birkedal (Copenhagen) Jens Blanck (Swansea) Steve Brookes (CMU) Bob Coecke (Oxford) Karl Crary (CMU) Martin Escardo (Birmingham) Achim Jung (Birmingham) Jean Krivine (LIX) James Laird (Sussex) Paul Levy (Birmingham) Catherine Meadows (NRL) Michael Mislove (Tulane) Catuscia Palamidessi (INRIA) Prakash Panangaden (McGill) Alex Simpson (Edinburgh) Christopher Stone (Harvey Mudd) Thomas Streicher (Darmstadt) James Worrell (Oxford) from submissions received in response to this Call for Papers. Submissions Now Open! Authors can submit papers in response to this Call for Papers by pointing their browser to http://www.easychair.org/conferences/?conf=mfps24 The submission process requires registering as an author and submitting the title and a short abstract for your paper by March 7, 2008. The deadline for submissions of full papers is one week later, March 14, 2008. The other important dates are listed below. Papers should be no more than 15 pages in LaTeX, and should be in the form of either a PostScript file or a pdf file suitable for printing on a generic printer. The accepted papers will appear in ENTCS, and the required format for ENTCS can be used for submissions. The generic ENTCS macro package can be found at this web site. There is no special entcsmacro.sty file for this year's MFPS Proceedings as yet; authors who use the ENTCS macros should just use the file that comes in the generic package. IMPORTANT DATES: * Fri Mar 7: Paper registration deadline, with short abstracts. * Fri Mar 14: Paper submission deadline. * Fri Apr 7: Author notification. * Fri Apr 21: Final versions for the proceedings.

1 0

position at Utrecht
by moerdijk＠math.uu.nl 21 Feb '08

21 Feb '08

Dear colleagues, I'd like to draw your attention to an opening for a tenure (track) position at Utrecht, at the level of "universitair docent" (comparable to Lecturer in the UK, Assistant Professor in the US or Maitre de Conferences in France). The position is related to a large group grant in the area between (and including) geometry/topology and mathematical physics, which I'm sure will fit the interests of many readers of this list. For more information, see http://www.math.uu.nl/Main/Department/Positions/ It is vacancy #62800 on the list of four. With best regards, Ieke Moerdijk. --

1 0

Clifford Lectures 2008
by Michael Mislove 20 Feb '08

20 Feb '08

Dear Colleagues, This is an invitation to attend the 2008 Clifford Lectures, which will be held at Tulane from March 12 through March 15, 2008. The Clifford Lectures are annual series of lectures hosted by the Tulane Math Department in honoring of A. H. Clifford, noted algebraist, who was a long time member of the department. This year's Clifford Lecturer is Samson Abramsky, and the topic of his lectures is, "Information flow in physics, geometry, logic and computation". Samson will deliver five lectures on this topic during the course of the series. In addition, thirteen researchers are also giving one-hour lectures on this topic as part of the series. You can find details about the speakers, the titles and abstracts of their talks, the program and registration information at the page http://www.math.tulane.edu/~mwm/clifford Best regards, Mike Mislove =============================================== Professor Michael Mislove Phone: +1 504 862-3441 Department of Mathematics FAX: +1 504 865-5063 Tulane University URL: http://www.math.tulane.edu/~mwm New Orleans, LA 70118 USA ===============================================

1 0

pssl87 - final announcement
by Panagis Karazeris 20 Feb '08

20 Feb '08

Peripatetic Seminar on Sheaves and Logic 87 Honouring the 70th birthday of Anders Kock Patras, 21-23 March 2008 The 87th Peripatetic Seminar on Sheaves and Logic will be held in Patras, Greece, on 22-23 March 2008. An extra session will be held in the afternoon of Friday 21 March, celebrating the 70th birthday of Anders Kock. A. Joyal, F. W. Lawvere and G. Reyes will participate honouring Anders. Accommodation Information: The University of Patras is located in the suburbs, 10 km NE of the downtown area. The participants have the options of either staying downtown or in one of the hotels along the coast near the University. In the first case they will have to use local transportation (bus or taxi). In the second case they may choose to walk (weather permitting) or get a ride by the people involved in the organization. With the second option in mind, a number of rooms has been reserved at Hotel Achaia Beach and will be available at the price of 69 Euros (single room) and 85 Euros (double room), provided that reservation is confirmed before 15 January 2008. The hotel is 2,5 km away from the PSSL venue and has the extra advantage of being close to some fine restaurants and in walking distance from the cafes, bars and restaurants of the coast of Rion, which starts getting lively at that time of the year. A small number of rooms will be available until Friday 22 February 2008. If you wish to book a hotel room yourself you may consult http://www.tripadvisor.com/Hotels-g189488-Patras_Peloponnese-Hotels.html Registration: You may register for PSSL87 by filling out the following form REGISTRATION FORM Name: ....... Affiliation: ..... I wish to give a talk: YES/NO Title: ..... Arrival Date: .... Departure Date: .... I wish to book a hotel room in Achaia Beach Hotel: YES/NO - SINGLE/DOUBLE and submitting it to pssl87(a)math.upatras.gr Transportation Information: Patras is located 220km W of the Athens airport. The best way to approach it is to use the Athens Suburban Railway (Proastiakos) which stretches west up to the town of Kiato, on the northern coast of the Peloponnese, 110km away from Patras. The idea is to arrange some private car or coach rides from Kiato to Patras, according to the date and time of arrival of most of you. Otherwise there is the option of getting on the (slow, narrow gauge) train to Patras. Further details as well as a list of participants appear in the meeting's webpage http://www.math.upatras.gr/~pssl87/

1 0

a monad
by Martin Escardo 18 Feb '08

18 Feb '08

Have you come across the following strong monad? Until I learn that it already has a name, I'll temporarily call it the selection monad, and denote it by S = (S,mu,eta). It is defined on an arbitrary cartesian closed category C after choosing an object V of C. Probably a monoidal closed category will do, but I haven't paused to consider this. On objects, define SX = X^(V^X) = ((X -> V) -> X). (One can contravariantly change the value object V, but I won't consider this in this message.) Think of elements of V^X as V-valued predicates, ranged over by p, and of elements of SX as selection functionals, ranged over by epsilon (like Hilbert's epsilon operator). Intuition: epsilon(p) picks an element x of X (perhaps among elements of a subset A of X) such that p(x) holds, if such an element exists. On morphisms f : X -> Y, define Sf: SX -> SY, using the lambda-calculus, with "\" as the notation for "lambda", and "o" for composition: Sf : SX -> SY epsilon |-> \p.f(epsilon(p o f)) This is easily seen to be functorial. Intuition: if epsilon selects elements among a subset A of X, then Sf(epsilon) selects elements among the set f(A). To do that, we first find an element x in A such that p(f(x)) holds, and then apply f to it. For the unit, take eta :: X -> SX x |-> \p.x Intuition: epsilon = eta(x) selects elements in the singleton set {x}, no matter which predicate p is given. For multiplication, take mu : S(S X) -> S X E |-> \p. E(\epsilon. p(epsilon p)) p Intuition: Given a selection operator E of selection operators, and given a predicate p, we select a selection operator epsilon, among the ones that E can select, such that epsilon selects an element x = epsilon(p) with p(x), and then apply such a selection operator to p to finally get such an element x. The unit and associativity laws are easily (but a bit laboriously) verified. This monad is strong, with strength t = t_{X,Y} defined by t : X x SY -> S(X x Y) (x, epsilon) |-> \p.(x, epsilon(\y.p(x,y))) Intuition: if epsilon selects elements among a subset B of Y, then t(x,epsilon) selects elements among the set {x} x B. This of course, using the monad structure and cartesian closedness, extends to a map times : SX x SY -> S(X x Y) Intuition: if epsilon_X and epsilon_Y select elements among sets A and B, then times(epsilon_X,epsilon_Y) selects among elements of A x B. (I don't think the strength is commutative.) Of course, one is familiar with the "continuation" monad QX=V^(V^X). There is a monad morphism SX -> QX epsilon |-> \p. p(epsilon p) My question is: have you come across the strong monad S (and its relationship to the monad Q)? Of course, S has many interesting submonads for particular choices of V, which correspond to submonads of Q that have been considered. I carry on a bit further. Suppose our category C has a nno N=(N,s,0), and write x+1=sx. Then we can define a natural isomorphism cons = cons_X cons : X x X^N <---> X^N : (head,tail) with head(alpha)=alpha(0) and tail(alpha)(n)=alpha(n+1). Then, as is well known, the map (head,tail) is a final coalgebra for the functor (-) -> X x (-). I want to consider the composite mul = (S cons) o times, mul : SX x S(X^N) -> S(X^N) For a sequence alpha = epsilon_0, epsilon_1, epsilon_2 ... of epsilon operators in SX, we may attempt to define the infinitely iterated product mul(epsilon_0, mul(epsilon_1, mul(epsilon_2, ...) ... )) It turns out that, in particular categories of interest, with a suitable choice of V, this exists. Moreover, there is a unique functional that picks the product selection operator, given the selection operators for the components: prod : (SX)^N -> S(X^N) prod(cons(epsilon,alpha)) = mul(epsilon, prod alpha) or, equivalently, prod o cons = mul o (id x prod) and so this is a kind of algebra homomorphism. The odd thing is that cons is the inverse of the final coalgebra, and, for this particular situation, it is instead playing the role of an initial algebra with respect to mul. (Of course, we are all familiar with odd situations of this kind.) There is no reason why such a unique morphism prod should exist in an arbitrary ccc with a chosen V, and counter-examples are readily obtained. My original example of prod was constructed before I realized there was a monad behind it, and was given by a construction that now can be considered to be rather ad hoc, but that is readily seen to be equivalent to the above formulation. So this message is a sort of apology for overlooking obvious considerations. The example was given in a ccc of computable higher-type functionals (defined on continuous functionals), with V the booleans, and, the point, was indeed, that prod is well defined and computable. I had considered another (more efficient) product functional, based on (seeing sequences as) binary trees. This also is explained, in very much the same (and obvious) way, by the above considerations, but I won't spell it down in this message, which is already long. To compare it with the ad hoc algorithms, I have coded the above categorical definitions in the higher-type programming language Haskell, including the definition of prod derived from them, for both sequences and trees. The performance in particular examples is the same as that of the ad hoc previously given algorithms, apart from a constant factor of approximately 1/2. I could, in principle, have started from the categorical ideas of this message and then derived the algorithms. I wish I had done that. In any case, here are the algorithms as they are derived in this message (including the tree-like product functional): http://www.cs.bham.ac.uk/~mhe/papers/selection-monad.hs MHE.

1 0

Finite limits in a category of free modules over a semiring
by Jamie Vicary 17 Feb '08

17 Feb '08

Dear category theorists, Given a commutative semiring R, construct the category that has nonnegative integers as objects, and matrices with entries in R as morphisms, such that the hom-set from N to M consists of matrices with M rows and N columns. This is then just the category of finitely-generated free R-modules. It admits a symmetric monoidal structure given by tensor product of modules, and has finite biproducts, with the induced CMon-enrichment agreeing with addition in R. Is there a nice way to characterise the semirings R for which this category has binary equalisers, and hence all finite limits? Note that the category is equal to its opposite, identifying each matrix with its transpose, and so it will have finite colimits iff it has finite limits. Also, we assume that our semiring has a 0 and a 1, is distributive, and that x.0=0.x=0 for all x in R. Jamie. PS: There was a interesting discussion of this towards the end of this page: http://golem.ph.utexas.edu/category/2007/11/geometric_representation_theor_…

2 1

Uniformity via Cauchy filters?
by Jeff Egger 13 Feb '08

13 Feb '08

Dear categorists, One of my current research projects has drifted into the realm of uniform locales, which is not exactly my forte. As I went to re-familiarise myself with the assorted definitions, I found myself wondering whether one could define a uniform locale as a locale equipped with a designated set of Cauchy filters, instead of uniform covers, or entourages. Does anyone know whether this idea has already been pursued, either for locales or for spaces? Cheers, Jeff. Looking for the perfect gift? Give the gift of Flickr! http://www.flickr.com/gift/

4 4

Call for Participation RELMICS10/AKA5
by Bernhard Möller 13 Feb '08

13 Feb '08

[Apologies for multiple copies.] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % Call for Participation % % % % RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 10th International Conference on Relational Methods in Computer Science (RelMiCS10) joint with 5th International Conference on Applications of Kleene Algebra (AKA5) 7-11 April 2008 Frauenwörth (near Munich), Germany http://www.uni-augsburg.de/rel_aka The RelMiCS Conference is the main forum for the relational calculus as a conceptual and methodological tool. The AKA Conference is a meeting on topics related to Kleene algebras. As in previous years, the two events are co-organised; they have a joint programme committee and joint proceedings. Registration deadline: 15 March 2006 PROGRAMME: The conference features 2 invited talks and 26 contributed papers. In addition, there is a PhD programme with 3 invited tutorial and 8 contributed talks; participation is open for everyone. Invited Talks: Marc Pauly (Standford) Formal Methods and the Theory of Social Choice Gunther Schmidt (Munich) Relations Making Their Way From Logics to Mathematics and Applied Sciences The full programme as well as registration details are available at the conference website. For further inquiries please contact the local organisers under rel_aka08(a)informatik.uni-augsburg.de. SPONSORS: ARIVA.DE AG (Kiel) CrossSoft (Kiel) Deutsche Forschungsgemeinschaft DFG HSH Nordbank AG (Kiel) COMMITTEES: General Chair: Rudolf Berghammer, Kiel, Germany Bernhard Moeller, Augsburg, Germany Local Organisation: Bernhard Moeller, Augsburg, Germany Roland Glueck, Augsburg, Germany Peter Hoefner, Augsburg, Germany Iris Kellner, Augsburg, Germany Ulrike Pollakowski, Kiel, Germany Programme Committee: Rudolf Berghammer, Kiel, Germany Harrie de Swart, Tilburg, The Netherlands Jules Desharnais, Laval, Canada Marcelo Frias, Buenos Aires, Argentina Hitoshi Furusawa, Kagoshima, Japan Peter Jipsen, Chapman, USA Wolfram Kahl, McMaster, Canada Yasuo Kawahara, Kyushu, Japan Bernhard Moeller, Augsburg, Germany Carroll Morgan New South Wales, Australia Manuel Ojeda Aciego, Málaga, Spain Ewa Orlowska, Warsaw, Poland Susanne Saminger, Linz, Austria Gunther Schmidt, Munich, Germany Renate Schmidt, Manchester, UK Giuseppe Scollo, Catania, Italy Georg Struth, Sheffield, UK Andrzej Szalas, Linköping, Sweden Johan van Benthem, Amsterdam, The Netherlands Michael Winter, Brock U., Canada -- Prof. Dr. Bernhard Möller | http://www.informatik.Uni-Augsburg.DE/~moeller/ Institut für Informatik | Tel: ++49-821-598-2164 Universität Augsburg | Fax: ++49-821-598-2274 Universitätsstr. 14, D-86135 Augsburg, Germany

1 0

IMLA'08: Call for Papers
by Aleks Nanevski 12 Feb '08

12 Feb '08

Fourth Internation Workshop on Intuitionistic Modal Logic and Applications (IMLA'08) (http://www.cs.bham.ac.uk/~vdp/IMLA08.html) A LICS'08 affiliated workshop Pittsburgh, Pennsylvania, June 23, 2008 Constructive modal logics and type theories are of increasing foundational and practical relevance in computer science. Applications are in type disciplines for programming languages, and meta-logics for reasoning about a variety of computational phenomena. Theoretical and methodological issues center around the question of how the proof-theoretic strengths of constructive logics can best be combined with the model-theoretic strengths of modal logics. Practical issues center around the question which modal connectives with associated laws or proof rules capture computational phenomena accurately and at the right level of abstraction. This workshop will bring together designers, implementers, and users to discuss all aspects of intuitionistic modal logics and type theories. Topics include, but are not limited to: * applications of intuitionistic necessity and possibility * monads and strong monads * constructive belief logics and type theories * applications of constructive modal logic and modal type theory to formal verification, foundations of security, abstract interpretation, and program analysis and optimization * modal types for integration of inductive and co-inductive types, higher-order abstract syntax, strong functional programming * models of constructive modal logics such as algebraic, categorical, Kripke, topological, and realizability interpretations * notions of proof for constructive modal logics * extraction of constraints or programs from modal proofs * proof search methods for constructive modal logics and their implementations The workshop continues a series of previous LICS-affiliated workshops, which were held as part of FLoC'99, Trento, Italy and of FLoC'02, Copenhagen, Denmark. We solicit submissions on work in progress and on more mature results. Submissions should be extended abstracts of 5-10 pages sent in PostScript or PDF format to the program co-chair at aleksn(a)microsoft.com. IMPORTANT DATES: Submission: April 25, 2008 Notification: May 23, 2008 Final papers due: June 7, 2008 Workshop Date: June 23, 2008 It is planned to publish workshop proceedings as Electronic Notes in Theoretical Computer Science (ENTCS) or in CEURS, to be decided. Authors please use the generic ENTCS macro package at http://www.math.tulane.edu/~entcs. PROGRAM COMMITTEE: Gavin Bierman (Microsoft, UK) Valeria de Paiva (PARC, USA) Michael Mendler (Bamberg, DE) Aleks Nanevski (Microsoft, UK) Brigitte Pientka (McGill, CA) Eike Ritter (Birmingham, UK) INVITED SPEAKERS: Frank Pfenning (CMU, USA) Torben Brauner (Roskilde, RK) CONTACTS Valeria de Paiva Aleks Nanevski PARC, Palo Alto Research Center Microsoft Research paiva(a)parc.xeroc.com aleksn(a)microsoft.com

1 0