August 2015 - Categories - categories.org.au

Chen review
by pjf 01 Sep '15

01 Sep '15

Free Press Journal (India) August 28, 2015 Cakes, Custard & Category Theory - Culinary approach to maths LENGTH: 482 words New Delhi: Cooking can be an answer to simplifying mathematics, says a new book which tries to whet the appetite of maths whizzes and arithmophobes alike with recipes and puzzles. From simple numeracy to category theory ('the mathematics of mathematics'), maths crusader Eugenia Cheng prescribes easy recipes for understanding complex arithmetic in her book "Cake, Custard and Category Theory". Calling on a baker's dozen of entertaining, puzzling examples and mathematically illuminating culinary analogies - including chocolate brownies, iterated Battenberg cakes, sandwiches, Yorkshire puddings and Mobius bagels - Cheng tells readers why everyone should love maths. So what on earth does a recipe have to do with maths? "You might think that rice cookers are for cooking rice. This is true, but this same piece of equipment can be used for other things as well: making clotted cream, cooking vegetables, steaming a chicken. Likewise, maths is about numbers, but it's about many things as well - getting the right answer, putting ideas together and so on," she says in the book, published by Hachette India. According to Cheng, a senior lecturer in Pure Mathematics at the University of Sheffield, many people are either afraid of maths, or baffled by it, or both. "Or they were completely turned off it by their lessons at school. I understand this - I was completely turned off sport by my lessons at school, and have never really recovered. I was so bad at sport at school, my teachers were incredulous that anybody so bad at sport could exist. And yet I'm quite fit now, and I have even run the New York marathon," he writes. She says 'category theory' which can be thought of as the 'mathematics of mathematics' is about relationships, contexts, processes, principles, structures, cakes and custard. "Yes, even custard. Because mathematics is about drawing analogies including custard, cake, pie, pastry, doughnuts, bagels, mayonnaise, yoghurt, lasagne and sushi." Maths, according to Cheng, like recipes, has both ingredients and method. "And just as a recipe would be a bit useless if it omitted the method, we can't understand what maths is unless we talk about the way it is done, not just the things it studies," she says. Citing examples of cottage, shepherd and fishermen pies, she says all these are more or less the same with the only difference being the filling that is sitting underneath the mashed potato topping. In all these cases, the recipe is not a full recipe but a blueprint and one can insert own choice of fruit or meat or fillings. "This is also how maths works. The idea of maths is to look for similarities between things so that you only need one 'recipe' for many different situations. The key is that when you ignore some details, the situations become easier to understand, and you can fill in the variables later," she writes. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

2 1

Award ceremony of the first Newton da Costa prize of logic
by Universal Logic 29 Aug '15

29 Aug '15

Recently happened in Florianopolis, Brazil the award ceremony of the first Newton da Costa prize of logic. This is a prize that will be attributed every year to the best paper written by someone working in Brazil. The winner of Newton da Costa prize 2015 is Rodrigo Freire from the University of Brasilia for his paper "First-order logic and first-order function" which has just been published in the journal Logica Universalis http://link.springer.com/journal/11787/9/3/page/1 Besides the publication of his paper, the participation to an international event outside of Brazil was offered to the winner, it was the participation to UNILOG'2015 in Istanbul, Turkey http://www.uni-log.org/UNILOG2015-Congress We encourage every country to organize each year a prize of logic along the same scheme, choosing the name of a great logician of the country. This is useful to develop interaction between logicians in a given country, to make internationally known their work and in general to promote logic in the world. Interesting people are welcome to enter in touch with us. Details of the Newton da Costa prize of logic can be found here http://www.uni-log.org/newton-da-costa-prize.html Jean-Yves Beziau Founder and organizer of Newton da Costa Prize of Logic Vice-president of the Brazilian Society of Logic Editor in Chief - Logica Universalis [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

coherence for symmetric monoidal and (co)affine categories
by Paul Blain Levy 24 Aug '15

24 Aug '15

Dear all, Given a category C, define symm(C) to be the following category: - an object is a finite family [or finite sequence, if preferred] of C-objects - a morphism from (C_i | i in I) to (D_j | j in J) consists of an bijection f : I --> J and, for each i in I, a C-morphism C_i --> D_fi. Define coaff(C) likewise but with "injection" instead of "bijection". It seems to be folklore that (1) symm(C) is the free symmetric monoidal category on C (2) coaff(C) is the free coaffine category (symmetric monoidal category with initial unit) on C. In the special case where C is discrete, these statements follow from the coherence arguments in Mac Lane's "Natural associativity and commutativity" and Petric's "Coherence in substructural categories". But for general C, where are these statements proved? Paul -- Paul Blain Levy School of Computer Science, University of Birmingham http://www.cs.bham.ac.uk/~pbl [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

3 2

categories of models of cartesian PROPs
by John Baez 24 Aug '15

24 Aug '15

Hi - Here are two questions: Suppose you have a category with finite products, say T, and a symmetric monoidal category, say C. Let [T,C] be the category where objects are symmetric monoidal functors from T to C, morphisms are monoidal natural transformations. *1. What structure beyond a mere category does [T,C] automatically get in this sort of situation?* *2. What further structure do we get if C has some particular class of limits or colimits?* I haven't thought about this much. Even if T were just symmetric monoidal, I think [T,C] should get a symmetric monoidal structure due to "pointwise multiplication", just as the set of homomorphisms from one commutative monoid to another becomes a commutative monoid where fg(x) := f(x) g(x) Should [T,C] also have some sort of "comultiplication"? What extra benefits do we get from T being cartesian? Here's why I care: My student Brendan Fong wrote a masters' thesis about Bayesian networks, which he's trying to polish up and publish. In the new improved version, he'll associate to any Bayesian network a category with finite products, say T. This plays the role of a "theory". An assignment of probabilities to random variables consistent with this theory is a symmetric monoidal functor from T to C, where C is some symmetric monoidal category - but not cartesian! - category of probability measure spaces and stochastic maps. So, [T,C] plays the role of the "category of models of T in C". It would be nice to know the properties of [T,C] that follow instantly from what I've said, not reliant on any more detailed information about T and C. Best, jb [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

5 6

ETAPS 2016 call for papers
by Tarmo Uustalu 17 Aug '15

17 Aug '15

****************************************************************** CALL FOR PAPERS: ETAPS 2016 19th European Joint Conferences on Theory And Practice of Software Eindhoven, The Netherlands, 2-8 April 2016 http://www.etaps.org/2016 ****************************************************************** -- ABOUT ETAPS -- ETAPS is the primary European forum for academic and industrial researchers working on topics relating to software science. ETAPS, established in 1998, is a confederation of five main annual conferences, accompanied by satellite workshops. ETAPS 2016 is the nineteenth event in the series. -- MAIN CONFERENCES (4-7 April) -- * ESOP: European Symposium on Programming (PC chair Peter Thiemann, Universität Freiburg, Germany) * FASE: Fundamental Approaches to Software Engineering (PC chairs Perdita Stevens, University of Edinburgh, UK, and Andrzej Wasowski, IT University of Copenhagen, Denmark) * FOSSACS: Foundations of Software Science and Computation Structures (PC chairs Bart Jacobs, Radboud Universiteit Nijmegen, The Netherlands, and Christof Löding, RWTH Aachen, Germany) * POST: Principles of Security and Trust (PC chairs Frank Piessens, Katholieke Universiteit Leuven, Belgium, and Luca Viganò, King's College London, UK) * TACAS: Tools and Algorithms for the Construction and Analysis of Systems (PC chairs Marsha Chechik, University of Toronto, Canada, and Jean-François Raskin (Université Libre de Bruxelles, Belgium) TACAS '16 hosts the 5th Competition on Software Verification (SV-COMP). -- INVITED SPEAKERS -- * Unifying speakers: Andrew D. Gordon (MSR Cambridge and University of Edinburgh, UK) Rupak Majumdar (MPI Kaiserslautern, Germany) * ESOP invited speaker: Cristina Lopes (University of California at Irvine, USA) * FASE invited speaker: Oscar Nierstrasz (Universität Bern, Switzerland) * POST invited speaker: Vitaly Shmatikov (University of Texas at Austin, USA) -- IMPORTANT DATES -- * 9 October 2015: Submission deadline for abstracts * 16 October 2015: Submission deadline for full papers * 2-4 December 2015: Author response period (ESOP and FoSSaCS only) * 18 December 2015: Notification of acceptance * 8 January 2016: Camera-ready versions due -- SUBMISSION INSTRUCTIONS -- ETAPS conferences accept two types of contributions: research papers and tool demonstration papers. Both types will appear in the proceedings and have presentations during the conference. ESOP and FoSSaCS accept only research papers. A condition of submission is that, if the submission is accepted, one of the authors attends the conference to give the presentation. Submitted papers must be in English presenting original research. They must be unpublished and not submitted for publication elsewhere. In particular, simultaneous submission of the same contribution to multiple ETAPS conferences is forbidden. The proceedings will be published in the Advanced Research in Computing and Software Science (ARCoSS) subline of Springer's Lecture Notes in Computer Science series. Papers must follow the formatting guidelines specified by Springer at the URL http://www.springer.de/comp/lncs/authors.html and be submitted electronically in pdf through the EasyChair author interface of the respective conference. Submissions not adhering to the specified format and length may be rejected immediately. FASE will try a light-weight double-blind review process (see http://www.etaps.org/2016/fase) - Research papers FASE, FOSSACS and TACAS have a page limit of 15 pp (excluding bibliography of max 2 pp) for research papers, whereas POST allows at most 20 pp (excluding bibliography of max 2 pp) and ESOP 25 pp (excluding bibliography of max 2 pp). Additional material intended for the referees but not for publication in the final version - for example, details of proofs - may be placed in a clearly marked appendix that is not included in the page limit. ETAPS referees are at liberty to ignore appendices and papers must be understandable without them. In addition to regular research papers, TACAS solicits also case study papers (at most 15 pp, excluding bibliography of max 2 pp). Both TACAS and FASE solicit also regular tool papers (at most 15 pp, excluding bibliography of max 2 pp). - Tool demonstration papers Submissions should consist of two parts: * The first part, at most 4 pages, should describe the tool presented. Please include the URL of the tool (if available) and provide information that illustrates the maturity and robustness of the tool. (This part will be included in the proceedings.) * The second part, at most 6 pages, should explain how the demonstration will be carried out and what it will show, including screen dumps and examples. (This part will be not be included in the proceedings, but will be evaluated. ESOP and FOSSACS do not accept tool demonstration papers. TACAS has a page limit of 6 pages for tool demonstrations. -- SATELLITE EVENTS (2-3 April, 8 April) -- Around 20 satellite workshops will take place before and after the main conferences. -- HOST CITY -- Eindhoven is located in the province of North Brabant in the south of the Netherlands. It is the fifth-largest city of the Netherlands. The city is well known for modern art, design and technology. The main airport of the Netherlands is the Amsterdam Airport, Schiphol. All major airlines fly to Schiphol, and Schiphol has a direct and very frequent train connection to Eindhoven. Eindhoven also has a small international airport, Eindhoven Airport, with direct connections to more than thirty destinations in Europe. -- HOST INSTITUTION -- ETAPS 2016 is hosted by Faculteit Wiskunde en Informatica, Technische Universiteit Eindhoven. -- ORGANIZERS * General chair: Jan Friso Groote * Workshops chair: Erik de Vink and Julien Schmaltz * Publicity chair: Anton Wijs -- FURTHER INFORMATION -- Please do not hesitate to contact the organizers at j.f.groote(a)tue.nl, a.j.wijs(a)tue.nl. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

HSCC 2016: Call for Papers
by Ichiro Hasuo 13 Aug '15

13 Aug '15

Dear colleagues, Please find below a CfP for HSCC 2016, a conference devoted to the study of hybrid systems (with both discrete and continuous dynamics). The topic might seem out of the scope of the categories list, but there have been exciting examples of "transfer" of results and ideas from the discrete world to the hybrid one, exploiting the abstraction power of the categorical language. They include [Haghverdi, Tabuada and Pappas, Theoretical Computer Science, 2005] and [Jacobs, Theoretical Computer Science, 2000]. I believe there's a chance that category theory will help making self-driving cars way safer :-) All the best, Ichiro Hasuo http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ ================================================== 19th International Conference on Hybrid Systems: Computation and Control (HSCC) April 12-14, 2016, Vienna, Austria URL: http://www.cs.ox.ac.uk/conferences/hscc2016/ Important dates Abstract Submission deadline (required): October 8, 2015. (no extensions possible) Paper Submission deadline: October 23, 2015. (no extensions possible) Rebuttal phase: November 27 to December 4, 2015. Author notification: December 18, 2015. Camera-ready submission: TBA. Demos/posters submission deadline: TBA. Conference dates: April 12-14, 2016. Conference Scope Hybrid Systems: Computation and Control (HSCC) has long been the leading, single-track conference on foundations, techniques, and tools for analysis, verification, control, synthesis, implementation, and applications of dynamical systems that exhibit continuous and discrete (hybrid) dynamics. Applications deal broadly with cyber-physical systems (CPS), and include mixed signal circuits, robotics, large-scale infrastructure networks, as well as natural systems such as biochemical and physiological models. We solicit theoretical as well as applied research papers that present original work combining ideas from computer science and control systems. Topics of interest include, but are not limited to: - Design, synthesis, planning and control - Analysis, automated verification (Boolean or quantitative) - Certification, validation, and testing - Model building from data (via learning) and model simulation - Mathematical foundations, computability and complexity - Programming languages, specification formalisms - Software tool engineering and experimentation - Real-time and resource-aware control - Network science and control over networks - Applications in cyber-physical systems, and in particular: automotive, avionics, energy and power, mobile and autonomous robotics, medical devices, manufacturing, transportation, systems and synthetic biology, models for the life sciences, and other areas. HSCC 2016 will be held as part of the eighth Cyber Physical Systems Week (CPS Week), alongside the International Conference on Cyber-Physical Systems (ICCPS), the International Conference on Information Processing in Sensor Networks (IPSN), the Real-Time and Embedded Technology and Applications Symposium (RTAS), and CPS-related workshops. Special Issue: Authors of distinguished papers may be invited to submit an extended version of their work for possible publication in a special issue of a leading journal in the CPS research area. Best Student Paper Award: As established in the previous years, a best student paper award will be given to a contribution primarily authored by a student. Repeatability Evaluation: HSCC has a history of publishing strong papers emphasising computational contributions; however, subsequent re-creation of these computational elements is often challenging because details of the implementation are unavoidably absent in the paper. Authors of papers accepted to HSCC (in any track) that contain a computational component will be invited to participate in an optional repeatability evaluation process after final submission of the paper in February. Papers that pass will be highlighted at the conference and in the proceedings, and all submissions will receive confidential feedback from independent reviewers on any challenges faced in recreating the computational results. Further details will be posted at the conference web page. Submission Guidelines Submitted papers should present unpublished original research, not under review elsewhere. Regular papers: maximum 10 pages in the 10pt, two-column ACM format. Tool and Case Study papers: maximum 6 pages in the 10pt, two-column ACM format. Tool Papers should describe an implemented tool and its novel features. Case studies should present hybrid systems tools or techniques. Demo/posters: Maximum 2 pages. Demo/poster descriptions serve the sole purpose of selecting contributions for the demo and poster session and will not be published in the conference proceedings. Submissions Submissions of Regular, Tool and Case-Study papers should be made through the HSCC 2016 EasyChair submission website: https://easychair.org/conferences/?conf=hscc2016 Submissions deadline is October 23, 2015 - corresponding abstracts should be submitted by October 8, 2015. ACM templates can be found at: http://www.acm.org/sigs/publications/proceedings-templates Demo/poster submissions: The submission deadline will be announced sometime in the beginning of 2016. Submission will be through email to hscc2016(a)easychair.org with "HSCC demo/poster submission" in the subject line. Questions should be directed to the same address. Committees for HSCC 2016 Program Committee Chairs Alessandro Abate, University of Oxford, UK Georgios Fainekos, Arizona State University, USA Publicity Chair Sayan Mitra, Univ. of Illinois at Urbana Champaign, USA Repeatability Evaluation Chair Ian M. Mitchell, University of British Columbia, Canada Demo/Poster Chair James Kapinski, Toyota Motors, USA Program Committee Shun-ichi Azuma, Kyoto University, Japan Christel Baier, TU Dresden, Germany Ezio Bartocci, TU Vienna, Austria Calin Belta, Boston University, USA Spring Berman, Arizona State University, USA Mireille Broucke, University of Toronto, Canada Krishnendu Chatterjee, IST Austria, Austria Alessandro Cimatti, Fondazione Bruno Kessler, Italy Alessandro D'Innocenzo, University of L'Aquila, Italy Thao Dang, VERIMAG, France Jyotirmoy Deshmukh, Toyota Motors, USA Xu Chu Ding, United Technology Research Center, USA Alexandre Donzé, UC Berkeley, USA Martin Fränzle, University in Oldenburg, Germany Antoine Girard, University of Grenoble, France Ichiro Hasuo, University of Tokyo, Japan Jun-ichi Imura, Tokyo Institute of Technology, Japan Franjo Ivancic, Google NY, USA Taylor Johnson, UT Arlington, USA Agung Julius, Rensselaer Polytechnic institute, USA Sertac Karaman, MIT, USA Joost-Pieter Katoen, RWTH Aachen University, Germany Marta Kwiatkowska, University of Oxford, UK Jun Liu, University of Waterloo, Canada Daniele Magazzeni, King's College London, UK Manuel Mazo Jr, TU Delft, The Netherlands Sayan Mitra, Univ. of Illinois at Urbana Champaign, USA Jens Oehlerking, Robert Bosch GmbH, Germany Meeko Oishi, University of New Mexico, USA Necmiye Ozay, University of Michigan, USA Andreas Podelski, University of Freiburg, Germany Pavithra Prabhakar, Kansas State University, USA Maria Prandini, Politecnico di Milano, Italy Akshay Rajhans, The MathWorks, USA S Ramesh, General Motors R&D, India Sriram Sankaranarayanan, Univ. of Colorado, Boulder, USA Oleg Sokolsky, University of Pennsylvania, USA Herbert Tanner, University of Delaware, USA Ufuk Topcu, UT Austin, USA Ashuthosh Trivedi, IIT Bombay, India Jana Tumova, KTH, Sweden Verena Wolf, Saarland University, Germany Majid Zamani, Technical University of Munich, Germany Naijun Zhan, Chinese Academy of Sciences, PR China Paolo Zuliani, Newcastle University, UK Steering Committee Rajeev Alur, University of Pennsylvania, USA Werner Damm, OFFIS, Germany John Lygeros, ETH Zurich, Switzerland Oded Maler, Verimag, France Paulo Tabuada, UCLA, USA Claire Tomlin, University of California Berkeley, USA [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: Current Issues in the Philosophy of Practice of Mathematics & Informatics
by Patrik Eklund 11 Aug '15

11 Aug '15

On 2015-08-09 05:10, Fred E.J. Linton wrote: > Not wishing to broadcast my illiteracy in the matter ... > So I ask you now, in public, where my shame can be greatest: what do > you mean by "lativity"? Thank you, Fred, for your questions. We were actually nervously waiting for somebody to ask that question, so we will remember you always for having done that. In logic we typically have signatures, terms, sentences, structured sets of sentences, entailment, models, satisfactions, axioms, theories and proof calculi. We cannot e.g. define entailment before we have a notion of sentences, and we should not define sentences before we have a notion of terms. The latter is a bit more controversial. In first-order logic I would see P(x), where P is a "predicate symbol", as a term, and not as a sentence, whereas putting a quantifier in front of it, Ex.P(x), makes it no longer a term. This is why I have difficulties e.g. to accept that the two 'not's in expressions like "not Ex.P(x)" and "Ex.not P(x)" would be the same. I am starting to think they are only informal as symbols, a bit similar as Church said lambda is and informal symbol, so actually not part of the formal syntax. Am I wrong or am I wrong? In logic we indeed need a signature (sorts and operators) in order to construct the categorical object of terms. Construction is important. We need terms to categorically construct sentences, which appear because of a sentence functor not being extendable to a monad. Otherwise sentences are terms, aren't they, because then we could substitute sentences within sentences, and that does not comply with our traditional view of sentences. Traditional first-order pretty much doesn't care, and neither did Aristotle about these things. Aristotle's and first-order logic are therefore very "illative" and also very unsorted, I would like to add. You are not broadcasting illiteracy at all, and your shame couldn't even be small because no shame whatsoever is justified to exist, at least not on your side. There may, however, be some of it now or eventually on my side, but let us see what happens if/when/how this dialogue develops. It may indeed turn out that at least some members of this catlist will see me just as a devoted soldier "seeking the bubble reputation, even in the canon's mouth". When we were searching for a name describing what we try to explain, we wanted to be careful not to use a "reserved word" that is more easily misunderstood than not well understood. In the latter case, we thought we can always try to explain, as I am about to do now. In the former case it would be a differentiation, which is more tricky. So here goes. 'Lative' is related to motion, and more specifically, motion 'to' and 'from', so when terms appear in sentences, terms 'move into' sentence, and 'appear within' sentences. At the same time, sentences 'move away from' terms, and separates terms from sentences. In comparison, 'ablative' is motion 'away', and nominative is static. The lative locative case (casus) indeed represents "motion", whereas e.g. a vocative case is identification with address. We want to underline the need not to have "mixed bags", so that we can ensure that a term does not appear in the bag of sentences, or a structured set of sentences would appear in the bad of entailment. I shouldn't compare with waste sorting, because then somebody might say "Patrik Eklund said Kurt G??del didn't care about waste sorting". Obviously, I do respect the work of G??del, even if at the same time I do find his approach "illative". From categorical point of view, G??del also complies only with the underlying category of sets, but as we have shown (e.g. in http://www.sciencedirect.com/science/article/pii/S0165011413000997) we may have other underlying categories for the the term monad. The term constructor and the use of category theory as the metalanguage for logic is here important. Logic developed "hand-in-hand" with set theory and as being a metalanguage for category theory should then not be confused with the lativity of logic we explain using categorical notions. Let me also again underline that nomenclatures and classifications in health care is one of our motivation areas of examples and applications. Nomenclatures exist also elsewhere, but he ones appearing in health we find very motivating. At this point of our "research program" we believe we have a fair understanding of the lativity as related to signatures, terms and sentences, and we hope we have a fair intuition about how we now proceed to investigate the lativity of that with respect e.g. to to entailment and models. Thanks again, and indeed, possible shame in whatever form or magnitude is all mine. Best, Patrik [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

4 3

Current Issues in the Philosophy of Practice of Mathematics & Informatics
by Ralph Matthes 09 Aug '15

09 Aug '15

[why on the categories mailing list? some of the courses are strongly based on category theory, and it seems that quite some subscribers to this list are interested in connections between mathematics and philosophy] Dear colleagues, The thematic trimester CIPPMI "Current Issues in the Philosophy of Practice of Mathematics & Informatics" will be held from 4th April to 1st July 2016 at the Centre International de Math??matiques et d'Informatique de Toulouse (CIMI). This thematic trimester is organised by an interdisciplinary team of researchers in Mathematics, Philosophy, and Computer Science from the Institut de Math??matiques de Toulouse (IMT) & the Institut de Recherche en Informatique de Toulouse (IRIT). It will feature course sessions, workshops, and a thematic school on themes at the interface of Philosophy, Mathematics and Computer Science. You will find all relevant information on the website of the thematic trimester that will be regularly updated: http://www.cimi.univ-toulouse.fr/cippmi/en A mailing list allows you to receive the different announcements from CIPPMI: https://sympa.math.ups-tlse.fr/wws/info/cippmi You can register at http://www.cimi.univ-toulouse.fr/cippmi/fr/inscriptionregistration A funding for accommodation is available in priority for junior researchers and for some senior researchers without funding from their laboratory. For further information, please consult the page: http://www.cimi.univ-toulouse.fr/cippmi/fr/boursesgrants With apologies for cross-posting, best regards, the CIPPMI scientific organisation committee. --- Ralph Matthes IRIT (CNRS & Univ. Toulouse) http://www.irit.fr/~Ralph.Matthes/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

7 7

Jobs at the University of Leeds
by Nicola Gambino 04 Aug '15

04 Aug '15

Dear friends and colleagues, the University of Leeds is currently advertising two positions in Pure Mathematics: (1) University Academic Fellow in Pure Mathematics http://jobs.leeds.ac.uk/MAPMA1022 (2) Holders of External Fellowships in Pure Mathematics http://jobs.leeds.ac.uk/MAPMA1026 Please feel free to contact me if you wish to have more information. With best wishes, Nicola === Dr Nicola Gambino School of Mathematics University of Leeds E-mail: n.gambino(a)leeds.ac.uk [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Call for Papers: Models for Formal Analysis of Real Systems (MARS'15)
by Rob van Glabbeek 04 Aug '15

04 Aug '15

Second Call for Papers: Workshop on Models for Formal Analysis of Real Systems (MARS 2015) Affiliated With LPAR 20 November 23, 2015 Suva, Fiji http://hoefner-online.de/mars15/ Aim: Logics and techniques for automated reasoning have often been developed with formal analysis and formal verification in mind. To show applicability, toy examples or tiny case studies are typically presented in research papers. Since the theory needs to be developed first, this approach is reasonable. However, to show that a developed approach actually scales to real systems, large case studies are essential. The development of formal models of real systems usually requires a perfect understanding of informal descriptions of the system-sometimes found in RFCs or other standard documents-which are usually just written in English. Based on the type of system, an adequate specification formalism needs to be chosen, and the informal specification translated into it. Abstraction from unimportant details then yields an accurate, formal model of the real system. The process of developing a detailed and accurate model usually takes a large amount of time, often months or years; without even starting a formal analysis. When publishing the results on a formal analysis in a scientific paper, details of the model have to be skipped due to lack of space, and often the lessons learnt from modelling are not discussed since they are not the main focus of the paper. The workshop aims at discussing exactly these unmentioned lessons. Examples are: * Which formalism is chosen, and why? * Which abstractions have to be made and why? * How are important characteristics of the system modelled? * Were there any complications while modelling the system? * Which measures were taken to guarantee the accuracy of the model? The workshop emphasises modelling over verification. In particular, we invite papers that present full Models of Real Systems, which may lay the basis for future formal analysis. The workshop will bring together researchers from different communities that all aim at verifying real systems and are developing formal models for such systems. Areas where large models often occur are within networks, (trustworthy) systems and software verification (from byte code up to programming- and specification languages). An aim of the workshop is to present different modelling approaches and discuss pros and cons for each of them. SUBMISSION: Submissions must be unpublished and not be submitted for publication elsewhere. Contributions are limited to 8 pages EPTCS style (http://style.eptcs.org) (not counting the appendix), but shorter extended abstracts are welcome. Appendices (of arbitrary length) can be used to present all details of a formalised model; the appendices will be part of the proceedings. Submissions must be in English and submitted in PDF format via EasyChair (TBC). All submissions will be peer reviewed by at least three referees based on their novelty, relevance and technical merit. The proceedings will be published as part of the open access series Electronic Proceedings in Theoretical Computer Science (EPTCS). IMPORTANT DATES (AoE): * Submission of abstracts: Monday 24 August 2015 * Submission: Monday 31 August 2015 * Notification: Friday 9 October 2015 * Final version: Monday 2 November 2015 * Workshop: Monday 23 November 2015 PROGRAMME COMMITTEE: Rance Cleaveland (University of Maryland, USA) Hubert Garavel (INRIA, France) Rob van Glabbeek (co-chair) (NICTA, Sydney, Australia) Jan Friso Groote (co-chair) (Eindhoven University of Technology, The Netherlands) He Jifeng (East China Normal University, China) Holger Hermanns (Saarland University, Germany) Peter Hoefner (co-chair) (NICTA, Sydney, Australia) Gerald Holzmann (NASA/JPL, USA) Magnus Myreen (Chalmers University, Sweden) Viet Yen Nguyen (Fraunhofer IESE, Germany) Bill Roscoe (University of Oxford, UK) Pamela Zave (AT&T Laboratories, USA) PROGRAMME CHAIRS and WORKSHOP ORGANISERS: Rob van Glabbeek (NICTA, Sydney, Australia) Jan Friso Groote (Eindhoven University of Technology, The Netherlands) Peter Hoefner (NICTA, Sydney, Australia) CONTACT: mars15(a)cs.stanford.edu [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0