October 2015 - Categories - categories.org.au

type theory postdoc at Dalhousie University
by Peter Selinger 22 Jan '16

22 Jan '16

Dear colleagues, I invite applications for one postdoctoral position, starting between now and January 1, at Dalhousie University under my supervision. The successful applicant will work on a project entitled "Trusted Quantum Software via a Formally Verified Functional Quantum Programming Language". Specifically, the project will involve the design of a type system for a type-safe 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 (including categorical semantics) of the language, and eventually the formalization of some of this meta-theory in a proof assistant. Familiarity with type theory (especially dependent type theory), programming language design, and/or semantics will be a prerequisite for this postdoc. 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. Although the position will be held at Dalhousie University in Canada, it will be an asset if the candidate is able to travel, because I will be spending one semester in Germany and one semester in the U.S. next year, and ideally I would like the postdoc to be able to accompany me. Funding for the project comes from the U.S. Air Force Office of Scientific Research, and the research project will be part of a team effort also involving collaborators from Tulane, Stanford, Oxford, the University of Iowa, and the University of Pennsylvania. The nominal start date for the project is September 30, 2015 (yes, this is today!), so the start date can be immediately, or some time in the near future. The position is initially for 1 year, and can be extended for an additional year. The salary is CAD $60,000 per year. Interested applicants should contact Peter Selinger at selinger(a)mathstat.dal.ca as soon as possible, and in any case before October 21. 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/ ]

2 1

WRLA 2016: 1st Call for Papers
by Dorel Lucanu 29 Oct '15

29 Oct '15

======================== Call for Papers ================================= WRLA 2016 11th International Workshop on Rewriting Logic and its Applications An ETAPS 2016 satellite event Eindhoven, The Netherlands, April 2-3, 2016 ========================================================================== IMPORTANT DATES * Abstract deadline: January 6th 2016 * Submission deadline: January 10th 2016 * Author notification: February 14th 2016 * Workshop: Saturday April 2nd and Sunday April 3rd, 2016 AIMS AND SCOPE Rewriting is a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication, and interaction. It can be used for specifying a wide range of systems and languages in various application domains. It also has good properties as a metalogical framework for representing logics. Several successful languages based on rewriting (ASF+SDF, CafeOBJ, ELAN, Maude) have been designed and implemented. The aim of WRLA is to bring together researchers with a common interest in rewriting and its applications, and to give them the opportunity to present their recent work, discuss future research directions, and exchange ideas. The 2016 edition of WRLA will mark its 20th anniversary since its first edition in Asilomar, California, in 1996. The topics of the workshop include, but are not limited to: A. Foundations * foundations and models of rewriting and rewriting logic, including termination, confluence, coherence and complexity * unification, generalisation, narrowing, and partial evaluation * constrained rewriting and symbolic algebra * graph rewriting * tree automata * rewriting strategies * rewriting-based calculi and explicit substitutions B. Rewriting as a Logical and Semantic Framework * uses of rewriting and rewriting logic as a logical framework, including deduction modulo * uses of rewriting as a semantic framework for programming language semantics * rewriting semantics of concurrency models, distributed systems, and network protocols * rewriting semantics of real-time, hybrid, and probabilistic systems * uses of rewriting for compilation and language transformation C. Rewriting Languages * rewriting-based declarative languages * type systems for rewriting * implementation techniques * tools supporting rewriting languages D. Verification Techniques * verification of confluence, termination, coherence, sufficient completeness, and related properties * temporal, modal and reachability logics for verifying dynamic properties of rewrite theories * explicit-state and symbolic model-checking techniques for verification of rewrite theories * rewriting-based theorem proving, including (co)inductive theorem proving * rewriting-based constraint solving and satisfiability * rewriting-semantics-based verification and analysis of programs E. Applications * applications to logic, mathematics and physics * rewriting models of biology, chemistry, and membrane systems * security specification and verification * applications to distributed, network, mobile, and cloud computing * specification and verification of real-time, probabilistic, and cyber-physical systems * specifications and verification of critical systems * applications to model-based software engineering * applications to engineering and planning INVITED SPEAKERS TBA SUBMISSION We solicit submissions of regular papers, tool papers, and work-in-progress papers. Regular papers must contain original contributions, be clearly written, include appropriate references, and comparison with related work. They must be unpublished and not submitted simultaneously for publication elsewhere. Tool papers have to present a new tool, a new tool component, or novel extensions to an existing tool. They should provide a short description of the theoretical foundations with relevant citations, emphasise the design and implementation, and give a clear account of the tool's functionality. The described tools must be publicly available via the web. Work-in-progress papers present early-stage work or other types of innovative or thought-provoking work related to the topics of the workshop. The difference between work-in-progress and regular papers is that work-in-progress submissions represent work that has not reached yet a level of completion that would warrant the full-refereed selection process. We encourage researchers and practitioners to submit work-in-progress papers as this provides a unique opportunity for sharing valuable ideas, eliciting useful feedback on ongoing work, and fostering discussions and collaborations among colleagues. All submissions should be formatted according to the guidelines for Springer LNCS papers, and should be submitted electronically using EasyChair at https://easychair.org/conferences/?conf=wrla2016 Regular and work-in-progress papers should not exceed 15 pages including references. Tool papers can have a maximum of 6 pages including references and may have an appendix of up to 4 additional pages with usage details and tool demonstration. PUBLICATION All submissions will be evaluated by the program committee. Regular papers, tool papers, and work-in-progress papers that are accepted will be presented at the workshop and included in the pre-proceedings, which will be available during the workshop. Following the tradition of the last editions, it is expected the regular papers, tool papers, and invited presentations to be published as a volume in Springer???s Lecture Notes in Computer Science (LNCS) series to be distributed after the workshop. A special issue of the Journal of Logical and Algebraic Methods in Programming (JLAMP) will be devoted to extended versions of selected papers from WRLA 2016. PROGRAM COMMITTEE Kyungmin Bae, SRI International, USA Mark van den Brand, Eindhoven University of Technology, The Netherlands Roberto Bruni, University of Pisa, Italy Stefan Ciobaca, Alexandru Ioan Cuza University, Romania Manuel Clavel, IMDEA Software Institute, Spain Francisco Dur??n, Universidad de M??laga, Spain Joerg Endrullis, Vrije Universiteit Amsterdam, The Netherlands Santiago Escobar, Universidad Polit??cnica de Valencia, Spain Maribel Fern??ndez, King's College London, UK Kokichi Futatsugi, JAIST, Japan Thomas Genet, ISTIC/Universit?? de Rennes 1, France J??rgen Giesl, RWTH Aachen, Germany Deepak Kapur, University of New Mexico, USA Helene Kirchner, INRIA, France Alexander Knapp, Universitat Augsburg, Germany Alberto Lluch Lafuente, Technical University of Denmark, Denmark Dorel Lucanu, Alexandru Ioan Cuza University, Romania (chair) Salvador Lucas, Universidad Polit??cnica de Valencia, Spain Narciso Mart??-Oliet, Universidad Complutense de Madrid, Spain Jos?? Meseguer, University of Illinois at Urbana-Champaign, USA Ugo Montanari, University of Pisa, Italy Pierre-Etienne Moreau, Universit?? de Lorraine, France Vivek Nigam, Federal University of Para??ba, Brasil Kazuhiro Ogata, JAIST, Japan Peter ??lveczky, University of Oslo, Norway Miguel Palomino, Universidad Complutense de Madrid, Spain Christophe Ringeissen, INRIA-Lorraine Nancy, France Grigore Rosu, University of Illinois at Urbana-Champaign, USA Vlad Rusu, INRIA Lille Nord-Europe, France Ralf Sasse, ETH Zurich, Switzerland Traian-Florin Serbanuta, University of Bucharest, Romania Mark-Oliver Stehr, SRI International, USA Carolyn Talcott, SRI International, USA Martin Wirsing, Ludwig-Maximilians-Universit??t M??nchen, Germany CONTACT INFORMATION For more information, please contact the organizers dlucanu(a)info.uaic.ro or visit the workshop web page http://fmse.info.uaic.ro/events/WRLA2016/ . [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

not(CH) and cardinal inequality in the absence of LEM
by David Roberts 28 Oct '15

28 Oct '15

Dear all, 1) not(CH) I'm reacquainting myself with the proof using toposes that not(CH) is relatively consistent. There's one step that is not quite as I'd like it, and that is as follows. Let P be a poset with the countable chain condition and the double negation topology (or indeed any site where all covering sieves are generated by families that are at most countable), then for objects X,Y in the base topos S that are infinite (in the sense that N x X = X), having Epi(Y,X) = 0 in S implies that Epi(Y^,X^) = 0 in Sh(P). It seems to me that the proof, as recounted in Mac Lane--Moerdijk or Johnstone's Baby Elephant for instance, uses LEM, by assuming that Epi(Y^,X^) =/= 0 and showing that Epi(Y,X) =/= 0. I haven't thought this through, but it seems like it might be possible to rework things so that the proof in fact shows that from an isomorphism 0--> Epi(Y,X) one can show that any two maps Epi(Y^,X^) --> \Omega are equal, and hence since 0 --> Epi(Y^,X^) is a subobject, it must be an isomorphism. Has anyone thought about this before? Of course, the previous paragraph may be nonsense, I admit... 2) Cardinal inequality in the absence of LEM This does raise the related question as to what the definition or definitions of <, strict inequality of cardinalities (i.e. just sets), could be in the absence of LEM and still be useful. If one were to adopt the following: Definition: B < A if and only if there a mono B >--> A and a factorisation B >--> A' >--> A such that Epi(B,A') = 0. then---modulo the issue in part 1)---the existing proof of the preservation of inequalities of sets seems to work without the assumption the base topos is boolean (which is needed in the existing proof to find a retract A -->> A' ). In the presence of LEM the definition of < reduces to the usual one, but I don't see a good reason or philosophy to single out this particular definition over other potential definitions except that it is what the proof uses. Thoughts? Best regards, David [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 1

Workshop on Homotopy Type Theory and Univalent Foundations, Fields Institute, May 16-20, 2016
by Chris Kapulkin 19 Oct '15

19 Oct '15

Dear all, We are pleased to announce a Workshop on Homotopy Type Theory and Univalent Foundations to be held at the Fields Institute in Toronto, May 16-20, 2016. Registration is available at: http://www.fields.utoronto.ca/programs/scientific/15-16/homotopy-type/ Limited financial support will be available to help cover participants' travel and local expenses. Priority will be given to students and postdocs who do not have access to other sources of funding. To be considered for funding, please fill out the Funding Application Form which is a part of the online registration. Deadline to apply for funding is *February 28, 2016*. Program: Mini-courses Robert Harper (Carnegie Mellon University): Computational interpretation of the Univalence Axiom Daniel R. Licata (Wesleyan University): Cubical Type Theory Peter LeFanu Lumsdaine (Stockholm University): Homotopy-theoretic models of type theory Michael Shulman (University of San Diego): Synthetic Homotopy Theory Invited speakers Benedikt Ahrens (IAS, Princeton) Thorsten Altenkirch (University of Nottingham) Jeremy Avigad (Carnegie Mellon University) Emily Riehl (Johns Hopkins University) Michael Warren (HRL Laboratories) There will also be contributed talks, selected by the Organizing Committee. We are looking forward to seeing you in Toronto! Organizers: Dan Christensen, Rick Jardine, Chris Kapulkin [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

CMCS 2016 : Second Call for Papers
by fabio.zanasi＠ens-lyon.fr 16 Oct '15

16 Oct '15

Call for Papers 13th International Workshop on Coalgebraic Methods in Computer Science (CMCS'16) 2 - 3 April 2016, Eindhoven, the Netherlands http://www.coalg.org/cmcs16 Objectives and scope ------------------- Established in 1998, the CMCS workshops aim to bring together researchers with a common interest in the theory of coalgebras, their logics, and their applications. As the workshop series strives to maintain breadth in its scope, areas of interest include neighbouring fields as well. Topics of interest include, but are not limited to, the following: - The theory of coalgebras (including set theoretic and categorical approaches) - Coalgebras as computational and semantical models (for programming languages, dynamical systems, term rewriting, etc.) - Coalgebras in (functional, object-oriented, concurrent, and constraint) programming - Model checking, theorem proving and deductive verification using coalgebraic techniques - Coalgebraic data types, type systems and behavioural typing - Proof principles and (coinductive) definitions for coalgebras (e.g. with bisimulations or invariants) - Coalgebras and algebras - Coalgebraic specification and verification - Coalgebras and (modal) logic - Coalgebra and control theory (notably of discrete event and hybrid systems) - Coalgebra in quantum computing - Coalgebra and game theory - Tools exploiting colgebraic techniques Venue and event --------------- CMCS'16 will be held in Eindhoven, the Netherlands, co-located with ETAPS 2016 on 2 - 3 April 2016. Keynote Speaker --------------- Jiri Adamek, Braunschweig University of Technology, Germany Invited Speakers --------------- Andreas Abel, University of Gothenburg, Sweden Filippo Bonchi, CNRS/ENS Lyon, France Invited Tutorial Speakers ------------------------- There will be a special session on weighted automata, with invited tutorials by Borja Balle, Lancaster University, United Kingdom Alexandra Silva, University College London, United Kingdom Important dates --------------- Abstract regular papers 4 January 2016 Submission regular papers 13 January 2016 Notification regular papers 12 February 2016 Camera-ready copy 19 February 2016 Submission short contributions 22 February 2016 Notification short contributions 6 March 2016 Programme committee ------------------- Paolo Baldan, University of Padova, Italy Corina Cirstea, University of Southampton, United Kingdom Ugo Dal Lago, University of Bologna, Italy Ichiro Hasuo (chair), University of Tokyo, Japan Tom Hirschowitz, CNRS and University of Savoie, France Bart Jacobs, Radboud University Nijmegen, the Netherlands Shin-ya Katsumata, Kyoto University, Japan Bartek Klin, University of Warsaw, Poland Barbara Koenig, University of Duisburg-Essen, Germany Stefan Milius, FAU Erlangen-Nuernberg, Germany Matteo Mio, CNRS and ENS Lyon, France Rasmus Mogelberg, IT University of Copenhagen, Denmark Larry Moss, Indiana University, United States Fredrik Nordvall Forsberg, University of Strathclyde, United Kingdom Dirk Pattinson, Australian National University, Australia Daniela Petrisan, Radboud University Nijmegen, the Netherlands Jean-Eric Pin, CNRS and Paris Diderot University, France John Power, University of Bath, United Kingdom Jurriaan Rot, University of Leiden, the Netherlands Jan Rutten, CWI/Radboud University Nijmegen, the Netherlands Alexandra Silva, University College London, United Kingdom Joost Winter, University of Warsaw, Poland James Worrell, University of Oxford, United Kingdom Publicity chair --------------- Fabio Zanasi, ENS Lyon, France PC chair -------- Ichiro Hasuo, University of Tokyo, Japan Submission guidelines --------------------- We solicit two types of contributions: regular papers and short contributions. Regular papers must be original, unpublished, and not submitted for publication elsewhere. They should not exceed 20 pages in length in Springer LNCS style. Short contributions may describe work in progress, or summarise work submitted to a conference or workshop elsewhere. They should be no more than two pages. Regular papers and short contributions should be submitted electronically as a PDF file via the Easychair system at http://www.easychair.org/conferences/?conf=cmcs2016. The proceedings of CMCS 2016 will include all accepted regular papers and will be published post-conference as a Springer volume in the IFIP-LNCS series. Accepted short contributions will be bundled in a technical report. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

terminology of (co)algebras
by Jiri Adamek 10 Oct '15

10 Oct '15

Does anyone know who was the first author to speak about F-algebras and/or F-coalgebras where F is a mere endofunctor? Lambek proved his famous lemma without using any name for the objects. And Arbib and Manes proved a number of properties but used the word "F-dynamics". Thanks Jiri [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

2 1

IWIL-11 in Fiji, extended deadline
by Geoff Sutcliffe 07 Oct '15

07 Oct '15

11th International Workshop on the Implementation of Logics FINAL CALL FOR PAPERS Extended deadline: October 15, 2015. The 11th International Workshop on the Implementation of Logics will be held in November 2015 in conjunction with the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning in Suva, Fiji We are looking for contributions describing implementation techniques for and implementations of automated reasoning programs, theorem provers for various logics, logic programming systems, and related technologies. Topics of interest include, but are not limited to: + Propositional logic and decision procedures, including SMT + First-order and higher order logics + Non-classical logics, including modal, temporal, description, non-monotonic reasoning + Formal foundations for efficient implementation of logic + Data structures and algorithms for the efficient representation and processing of logical concepts + Proof/model search organization and heuristics for logical reasoning systems + Data analysis and machine learning approaches to search control + Techniques for proof/model search visualization and analysis + Practical constraint handling + Reasoning with ontologies and other large theories + Implementation of efficient theorem provers and model finders for different logics + System descriptions of logical reasoning systems + Issues of reliability, witness generation, and witness verification + Evaluation and benchmarking of provers and other logic-based systems + I/O standards and communication between reasoning systems We are particularly interested in contributions that help the community to understand how to build useful and powerful reasoning systems, and how to apply them in practice. Researchers interested in participating are invited to submit a position statement (2 pages), a short paper (up to 5 pages), or a full papers (up to 15 pages) via the EasyChair page for IWIL-2015, https://easychair.org/conferences/?conf=iwil2015 Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Submissions should be in standard-conforming PDF. Final versions will be required to be submitted in LaTeX using the easychair.cls class file. Proceedings will be published as EasyChair Proceedings. If number and quality of the submissions warrant it, we plan to produce a special issue of a recognized journal on the topic of the workshop. Important Dates: + Submission of papers/abstracts: October 12, 2015 (extended deadline) + Notification of acceptance: October 26, 2015 + Camera ready versions due: November 9, 2015 + Workshop: November 23, 2015 Program committee: + Boris Konev (Co-Chair) University of Liverpool + Stephan Schulz (Co-Chair) DHBW Stuttgart + Laurent Simon (Co-Chair) University of Bordeaux + Christoph Benzm??ller Freie Universit??t Berlin + Armin Biere Johannes-Kepler Universit??t Linz + Jasmin Blanchette INRIA/LORIA/Max-Planck-Institut f??r Informatik + Guillaume Burel ENSIIE/CEDRIC + Simon Cruanes INRIA Paris-Rocquencourt + Tommi Junttila Aalto University + Yevgeny Kazakov Universit??t Ulm + Konstantin Korovin University of Manchester + Albert Oliveras Universitat Polit??cnica de Catalunya + Jens Otten Universit??t Potsdam + Andrew Reynolds Ecole polytechnique f??d??rale de Lausanne + Peter Schneider-Kamp University of Southern Denmark + Geoff Sutcliffe University of Miami + Josef Urban Radboud University/Czech Technical University + Uwe Waldmann Max-Planck-Institut f??r Informatik Previous Workshops: + Reunion Workshop (held in conjunction with LPAR'2000 on Reunion Island) + Second Workshop (with LPAR 2001 in Havana, Cuba) + Third Workshop (with LPAR 2002 in Tbilisi, Georgia) + Fourth Workshop (with LPAR 2003 in Almati, Kazakhstan) + Fifth Workshop (with LPAR 2004 in Montevideo, Uruguay) + Sixth Workshop (with LPAR 2006 in Phnom Penh, Cambodia) + Seventh Workshop (with LPAR 2008 in Doha, Qatar) + Eighth Workshop (with LPAR 2010 in Yogyakarta, Indonesia) + Ninth Workshop (with LPAR 2012 in Merida, Venezuela) + Tenth Workshop (with LPAR 2013 in Stellenbosch, South Africa) [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Decision-making and Category theory
by Venkata Rayudu Posina 06 Oct '15

06 Oct '15

Dear All, Would you be kind enough to point me to literature (papers / books) on the applications of category theory to decision-making problems. Thanking you, Yours truly, posina [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

2 1

Announcement conference Stef Caenepeel 60
by Joost Vercruysse 02 Oct '15

02 Oct '15

Dear colleague, In 2016, Stef Caenepeel will turn 60. To celebrate this joyful event, a conference is organized in Turin, Italy, from Tue 24 - Fri 27 May 2016 entitled "Brauer groups, Hopf algebras and monoidal categories. -- A conference in honour of Stef Caenepeel on the occasion of his 60th birthday" Hereby, you are cordially invited to participate in this meeting. A (tentative) list of speakers can be found at the end of this message. A poster session is organized for PhD students and young post-docs who would like to present their results during the meeting. The conference website can be found on the address: http://homepages.vub.ac.be/~hopfalgb If you are interested to attend the conference, please fill out the registration form that is available on this site. Feel free to forward this message to everyone who might be interested. We hope to be welcoming you in Turin next May, Best wishes, The organizers, Ana Agore Alessandro Ardizzoni Sorin Dascalescu Isar Goyvaers Gigel Militaru Joost Vercruysse Tentative list of speakers: Jaques Alev Eliezer Batista Margaret Beattie Gabriella Böhm Tomasz Brzezinski Daniel Bulacu Frederik Caenepeel Mia Cohen Juan Cuadra Bojana Femic Timmy Fieremans José Gomez-Torrecillas Tomas Guédénon Miodrag Iovanov Bogdan Ion George Janelidze Eric Jespers Lars Kadison Lieven Lebruyn Tom Lenagan Andrei Marcus Claudia Menini Constantin Nastacescu Florin Panaite Peter Schauenburg Yorck Sommerhauser Dragos Stefan Alexander Stolin Blas Torecillas Fred Van Oystaeyen Alain Verschoren Yinhuo Zhang [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Faculty position in PL/verification/theorem-proving at Cambridge.
by Marcelo Fiore 02 Oct '15

02 Oct '15

Faculty position in PL/verification/theorem-proving at Cambridge [this is roughly analogous to a US tenured associate professor position] http://www.jobs.cam.ac.uk/job/8134/ The University of Cambridge Computer Laboratory is seeking to recruit a new faculty member at the Lecturer or Senior Lecturer level who can contribute to research in areas such as (but not limited to) the following: - theoretical foundations of programming - programming language design and implementation - formal specification and verification of computer systems - theorem proving and its application to hardware and software The ideal candidate will have interests that range from mathematical theory to practical applications and will demonstrate the potential to collaborate with Computer Laboratory research students, staff and faculty across a range of topics. Notwithstanding the above focus, exceptional candidates from any area of Computer Science are also encouraged to apply. It is likely that successful candidates will already have a strong track record in one or more relevant research areas and already have some postdoctoral experience. Ideally the candidate will also have experience of teaching and generating research grant income. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0