December 2016 - Categories - categories.org.au

Midlands Graduate School 2017, Leicester, UK
by Roy L. Crole 30 Dec '16

30 Dec '16

This is a preliminary announcement for *The Midlands Graduate School in the Foundations of Computing Science 2017* * April 9-13, Leicester, UK* ( http://www.cs.le.ac.uk/events/mgs2017/ ) The MGS has run very successfully for many years now, and in recent years we have had over 50 participants making for exciting and vibrant schools. We would be delighted to see you in Leicester in 2017. Please forward to all those you think will be interested! The organisers: Samuel Balco Roy Crole -- R. L. Crole Associate Professor Department of Informatics University Road University of Leicester Leicester LE1 7RH United Kingdom T: +44 (0)116 252 3404 E: rlc3(a)le.ac.uk W: www.cs.le.ac.uk/people/rlc3 Times Higher Awards Winner 2007-2015 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

10+ Open Positions in Tokyo: Formal Methods and Cyber-Physical Systems
by Ichiro Hasuo 21 Dec '16

21 Dec '16

[Thanks a lot for disseminating among potentially interested candidates. Apologies for multiple copies] Dear colleagues, For our new 5.5-year research project (ERATO MMSD, Metamathematics for Systems Design) we are looking for 10+ senior researchers and postdocs, together with research assistants (PhD students) and internship students. This broad project aims to extend the realm of formal methods from software to cyber-physical systems (CPS), with particular emphases on logical/categorical metatheories and industrial application (esp. in automotive industry). The project covers diverse areas that include: formal methods, programming languages, software science, software engineering, control theory, machine learning, numerical optimization, user interface, mathematical logic and category theory. For more about the project please visit http://www-mmm.is.s.u-tokyo.ac.jp/eratommsd/about.html About the open positions http://www-mmm.is.s.u-tokyo.ac.jp/eratommsd/openpositions.html has more information (esp. how to apply/inquire). Best regards, Ichiro ======= Ichiro Hasuo Dept. Computer Science, The University of Tokyo http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/ [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Two postdoc positions at Dalhousie
by Peter Selinger 16 Dec '16

16 Dec '16

This sender failed our fraud detection checks and may not be who they appear to be. Learn about spoofing at http://aka.ms/LearnAboutSpoofing Dear colleagues, I invite applications for two postdoctoral position, starting early in 2017 (ideally in January or February), at Dalhousie University under my supervision. The successful applicants will work on a project entitled "Trusted Quantum Software via a Formally Verified Functional Quantum Programming Language". Specifically, the project involves the design and semantics of a functional programming language for quantum computing, loosely modelled on the Quipper language (http://www.mathstat.dal.ca/~selinger/quipper/) It will also involve developing the meta-theory of the language, and eventually the formalization of some of this meta-theory in a proof assistant. The research project is part of a team effort, also involving collaborators from Tulane, Stanford, Oxford, the University of Iowa, and the University of Pennsylvania. Familiarity with type theory, programming language design, and/or semantics (including categorical semantics) will be a prerequisite for these postdocs. Familiarity with quantum computing will be helpful, but is neither necessary nor sufficient for this position - the main emphasis is on programming languages and type systems. The positions are initially for 1 year, and can be extended for an additional year. The salary is $50,000 Canadian per year plus benefits. Two positions are available: * Postdoc 1 is funded by the U.S. Air Force Office of Scientific Research. The postdoc will be held in the Department of Mathematics and Statistics at Dalhousie University. * Postdoc 2 is funded by Rigetti Computing, a quantum computing startup based in Berkeley, California (rigetti.com) The postdoc position is formally known as the "Rigetti Computing Prize Fellowship". The postdoc will be held in the Department of Mathematics and Statistics at Dalhousie University, but the applicant will be expected to spend three months per year on site at Rigetti Computing office in Berkeley to work on Rigetti projects related to quantum computing. Interested applicants should contact Peter Selinger at selinger(a)mathstat.dal.ca as soon as possible, and in any case before January 10. I can provide more details about the research project to interested applicants on request. Thanks, -- Peter [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

recent papers posted to arXiv
by Lucius Schoenbaum 15 Dec '16

15 Dec '16

Dear All, Some of you may have been pinged already, but I wanted to call attention to a pair of papers I have posted to the arXiv at the end of last week: https://arxiv.org/abs/1612.02816 [1] https://arxiv.org/abs/1612.02885 [2] The article [1] may be of interest to those interested in categorical logic. It describes a generalization of the Curry-Howard correspondence to a generalized setting, resembling a higher category. The second article [2] is connected in the sense that [1] motivates [2], and conversely [2] provides background that may be needed to read [1], but I am right on top of the project so it is hard for me to say. I would estimate this work is somewhere between "fresh" and "very fresh". So I would welcome your comments and critiques, and reports of any nits or sources of discomfort. Best to All Here, Lucius Schoenbaum [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Some recent advances in SDG
by Anders Kock 13 Dec '16

13 Dec '16

Dear all, Some of my recent contributions to SDG are posted on arXiv: 1) Most recently (Dec. 2016): "Metric spaces and SDG" (version 3) - a corrected version of a preprint posted on arxiv:1610.10005 version 1 and 2. (I apologize if anybody has wasted time with the puzzling redundancies and holes in the first two versions!) This preprint relates SDG with the theory of some metric spaces advanced by Busemann in the years 1943-1970 (and he called, quite justified, his theory "Synthetic Differential Geometry" !). 2) Also, I posted on arXiv:1508.04322, "Affine combinations in affine schemes": out of mutual neighbour points in an affine scheme, one can form arbitrary affine combinations. In a different context, this technique was used for many of the constructions in my book Synthetic Geometry of Manifolds (2010). 3) Finally, arXiv:1610.00286 is a survey talk "New methods for old spaces: synthetic differential geometry", presented as an invited contribution to the workshop (and forthcoming book) organized by M. Anel and G. Catren "New spaces in Mathematics and Physics", Paris IHP 2015. These three contributions concentrate on the combinatorial neighbour relation in geometry, and how it carries along with it diffenential-geometric notions, like "touching", "envelopes", ... - without resorting to differential calculus. Anders Kock [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

jobs at Macquarie
by Steve Lack 13 Dec '16

13 Dec '16

Dear Colleagues, Macquarie is currently advertising for three positions, including one 4-year position in Pure Mathematics, with people working in analysis, category theory, or PDEs particularly encouraged to apply. The other two positions are both continuing (the closest thing we have to tenure); one is in Applied Mathematics, the other is a teaching position. For more information follow the link http://jobs.mq.edu.au/cw/en/listing/ or feel free to contact me. Regards, Steve Lack. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

CALCO 2017: First Call for Papers
by Fabio Zanasi 07 Dec '16

07 Dec '16

========================================================= CALL FOR PAPERS: CALCO 2017 7th International Conference on Algebra and Coalgebra in Computer Science June 13 - 16, 2017 Ljubljana, Slovenia http://coalg.org/calco17/ ========================================================== Abstract submission: April 3, 2017 Paper submission: April 7, 2017 Author notification: May 15, 2017 Final version due: May 31, 2017 ========================================================== -- SCOPE -- CALCO aims to bring together researchers and practitioners with interests in foundational aspects, and both traditional and emerging uses of algebra and coalgebra in computer science. It is a high-level, bi-annual conference formed by joining the forces and reputations of CMCS (the International Workshop on Coalgebraic Methods in Computer Science), and WADT (the Workshop on Algebraic Development Techniques). Previous CALCO editions took place in Swansea (Wales, 2005), Bergen (Norway, 2007), Udine (Italy, 2009), Winchester (UK, 2011), Warsaw (Poland, 2013) and Nijmegen (the Netherlands, 2015). The seventh edition will be held in Ljubljana, Slovenia, colocated with MFPS XXXIII. -- INVITED SPEAKERS -- Nicoletta Sabadini - University of Insubria, IT Alex Simpson - University of Ljubljana, SL James Worrell - University of Oxford, UK (joint with MFPS) Catuscia Palamidessi - Ecole polytechnique, FR (joint with MFPS) Vincent Danos - Ecole normale superieure, FR (joint with MFPS) Marco Gaboardi - University at Buffalo, USA (joint with MFPS) -- SPECIAL SESSION ON METRICS, PRIVACY AND LEARNING -- (joint event with MFPS) -- TOPICS OF INTEREST -- We invite submissions of technical papers that report results of theoretical work on the mathematics of algebras and coalgebras, the way these results can support methods and techniques for software development, as well as experience with the transfer of the resulting technologies into industrial practice. We encourage submissions in topics included or related to those listed below. * Abstract models and logics - Automata and languages - Categorical semantics - Modal logics - Relational systems - Graph transformation - Term rewriting * Specialised models and calculi - Hybrid, probabilistic, and timed systems - Calculi and models of concurrent, distributed, mobile, and context-aware computing - General systems theory and computational models (chemical, biological, etc.) * Algebraic and coalgebraic semantics - Abstract data types - Inductive and coinductive methods - Re-engineering techniques (program transformation) - Semantics of conceptual modelling methods and techniques - Semantics of programming languages * System specification and verification - Algebraic and coalgebraic specification - Formal testing and quality assurance - Validation and verification - Generative programming and model-driven development - Models, correctness and (re)configuration of hardware/middleware/architectures, - Process algebra * Corecursion in Programming Languages - Corecursion in logic / constraint / functional / answer set programming - Corecursive type inference - Coinductive methods for proving program properties - Implementing corecursion - Applications * Algebra and Coalgebra in quantum computing - Categorical semantics for quantum computing - Quantum calculi and programming languages - Foundational structures for quantum computing - Applications of quantum algebra * String Diagrams and Network Theory - Combinatorial approaches - Theory of PROPs and operads - Rewriting problems and higher-dimensional approaches - Automated reasoning with string diagrams - Applications of string diagrams - Connections with Control Theory, Engineering and Concurrency -- SUBMISSION GUIDELINES -- Prospective authors are invited to submit full papers in English presenting original research. Submitted papers must be unpublished and not submitted for publication elsewhere. Experience papers are welcome, but they must clearly present general lessons learned that would be of interest and benefit to a broad audience of both researchers and practitioners. Proceedings will be published in the Dagstuhl LIPIcs???Leibniz International Proceedings in Informatics series. Final papers should be no more than 15 pages long in the format specified by LIPIcs (http://www.dagstuhl.de/publikationen/lipics/anleitung-fuer-autoren/) It is recommended that submissions adhere to that format and length. Submissions that are clearly too long may be rejected immediately. Proofs omitted due to space limitations may be included in a clearly marked appendix. Both an abstract and the full paper must be submitted by their respective submission deadlines. A special issue of the open access journal Logical Methods in Computer Science (http://www.lmcs-online.org) containing extended versions of selected papers, is also being planned. Submissions will be handled via EasyChair https://www.easychair.org/conferences/?conf=calco2017 -- BEST PAPER AND BEST PRESENTATION AWARDS -- This edition of CALCO will feature two awards: a Best Paper Award whose recipients will be selected by the PC before the conference and a Best Presentation Award, elected by the participants. -- IMPORTANT DATES -- Abstract submission: April 3, 2017 Paper submission: April 7, 2017 Author notification: May 15, 2017 Final version due: May 31, 2017 -- PROGRAMME COMMITTEE -- Andrej Bauer (University of Ljubljana, Slovenia) Filippo Bonchi (ENS Lyon, France, co-chair) Marcello Bonsangue (University of Leiden, Netherlands) Corina Cirstea (University of Southampton, UK) Robin Cockett (University of Calgary, Canada) Andrea Corradini (University of Pisa, Italy) Sergey Goncharov (Universitaet Erlangen-Nuernberg, Germany) Helle Hvid Hansen (Delft University of Technology, Netherlands) Ichiro Hasuo (University of Tokyo, Japan) Tobias Heindel (University of Copenhagen, Denmark) Tom Hirschowitz (Savoie Mont Blanc University, France) Bart Jacobs (University of Nijmegen, Netherlands) Bartek Klin (Warsaw University, Poland) Barbara Koenig (University of Duisburg-Essen, Germany, co-chair) Alexander Kurz (University of Leicester, UK) Paul Levy (University of Birmingham, UK) Radu Mardare (Aalborg University, Denmark) Stefan Milius (Universitaet Erlangen-Nuernberg, Germany) Samuel Mimram (Ecole Polytechnique, France) Till Mossakowski (Universitaet Magdeburg, Germany) Larry Moss (Indiana University, US) Daniela Petrisan (Universite Paris-Diderot, France) John Power (University of Bath, UK) Grigore Rosu (University of Illinois, US) Jan Rutten (CWI, University of Nijmegen, Netherlands) Peter Selinger (Dalhousie University, Canada) Alexandra Silva (University College London, UK) Pawel Sobocinski (University of Southampton, UK) Ana Sokolova (University of Salzburg, Austria) -- ORGANISING COMMITTEE -- Andrej Bauer (University of Ljubljana, Slovenia) Matija Pretnar (University of Ljubljana, Slovenia) -- PUBLICITY CHAIR -- Fabio Zanasi (University College London, UK) -- SATELLITE WORKSHOPS: CALCO EARLY IDEAS AND CALCO TOOLS -- The CALCO Early Ideas Workshop is intended to enable presentation of work in progress and original research proposals. PhD students and young researchers are particularly encouraged to contribute. The CALCO Tools Workshop is dedicated to tools based on algebraic and/or coalgebraic principles. CALCO 2017 will run together with the CALCO Early Ideas Workshop, with dedicated sessions at the end of each conference day. CALCO Tools will take place on June 13. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Fibred 2-category of Grothendieck toposes?
by Steve Vickers 06 Dec '16

06 Dec '16

If "Grothendieck topos" means bounded geometric morphism into a given base S, then by allowing the base to vary we can get a 2-category GTop of Grothendieck toposes, fibred over some form of ETop (elementary toposes). This is because pseudopullbacks of bounded geometric morphisms along arbitrary geometric morphisms exist and are still bounded. (I say "some form of" ETop because it may be better to restrict the 2-cells downstairs to be isos, even though we certainly don't want to do the same upstairs. Also nnos are needed if classifying toposes are to exist.) Has anyone worked on that particular combination of bounded and unbounded? Steve Vickers. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

3 2

Re: Fibred 2-category of Grothendieck toposes?
by Thomas Streicher 05 Dec '16

05 Dec '16

Dear Steve, > How shall we wrap this up? the point is that postcomposition with a gm F-|U is tanatamount to change of base long F. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Re: Fibred 2-category of Grothendieck toposes?
by Steve Vickers 05 Dec '16

05 Dec '16

Dear Thomas, How shall we wrap this up? 1. Do you agree that the structure I was aiming for was correct for my intended applications? As you say, the pseudo-pullbacks of bgms are already in the Elephant, though I think there are still 2-categorical details to be dealt with in order to make that indexed. I believe I have done that with a fibred 2-category along the lines of Buckley's paper. My original question was to see if anyone else had gone in a similar direction. 2. Why are algebraic and geometric reindexing given by pre- and post-composition? My reading is that "algebraic" is composition, "geometric" is pullback. 3. What's your understanding of "change of base" here? The prototype example is the codomain fibration, where the base change morphisms between slices are given by pullback. What that does within an elementary topos translates into what I was doing restricted to BTop, the fibre over S being just the slice (of bgms with codomain S). All the best, Steve. > On 4 Dec 2016, at 12:00, Thomas Streicher <streicher(a)mathematik.tu-darmstadt.de> wrote: > > Steve, > > we are speaking about different things. Pullbacks of bgm's along > arbitrary gm's are described sufficiently well [Joh77] and in the > Elephant. > > But what I have commented on was how to appropriately captured change > of base when studying topose sover a base topos. > > I am working on the "algebraic" side whereas you think on the > "geometric" side. Reindexing in terms of the algebraic view is given > by precomposition but reindexing in terms of the geometric view is > postcomposition. > > What I want to say is that pullbacks in Top are very different from > the change of base for relative topos theory. > > Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0