June 2018 - Categories - categories.org.au

Homotopy of singular simplicial set
by Michael Barr, Prof. 10 Jun '18

10 Jun '18

Does anyone have a reference for the fact that homotopic maps between topological spaces induce homotopies between the singular simplicial complexes on those spaces. I am interested in explicit formulas. Michael [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

how should I implement production of Category ?
by xieyuheng 07 Jun '18

07 Jun '18

if I implement Category as idris interface, how should I implement production of Category ? it seems like a function take two interfaces and return an interface, thus interface need to be first class object to implement production this way. my repo of Category is here :: https://github.com/xieyuheng/idris-category/blob/master/Category.idr [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Mathematically Structured Functional Programming 2018: Call for Participation
by Robert Atkey 04 Jun '18

04 Jun '18

Seventh Workshop on MATHEMATICALLY STRUCTURED FUNCTIONAL PROGRAMMING Sunday 8th July 2018, Oxford, UK A satellite workshop of FSCD 2018 http://msfp2018.bentnib.org/ CALL FOR PARTICIPATION Registration: ============ Register here: http://www.floc2018.org/register/ Early registration deadline: Wednesday 6th June Invited Speakers: ================= - Tamara von Glehn, University of Cambridge, UK - Didier Remy, INRIA, France The seventh workshop on Mathematically Structured Functional Programming is devoted to the derivation of functionality from structure. It is a celebration of the direct impact of Theoretical Computer Science on programs as we write them today. Modern programming languages, and in particular functional languages, support the direct expression of mathematical structures, equipping programmers with tools of remarkable power and abstraction. Where would Haskell be without monads? Functional reactive programming without temporal logic? Call-by-push-value without adjunctions? The list goes on. This workshop is a forum for researchers who seek to reflect mathematical phenomena in data and control. The first MSFP workshop was held in Kuressaare, Estonia, in July 2006, affiliated with MPC 2006 and AMAST 2006. The second MSFP workshop was held in Reykjavik, Iceland as part of ICALP 2008. The third MSFP workshop was held in Baltimore, USA, as part of ICFP 2010. The fourth workshop was held in Tallinn, Estonia, as part of ETAPS 2012. The fifth workshop was held in Grenoble, France, as part of ETAPS 2014. The sixth MSFP Workshop was held in April 2016, in Eindhoven, Netherlands, just after ETAPS 2016. Programme: ========== See also https://easychair.org/smart-program/FLoC2018/MSFP-program.html for abstracts. 09:00 Invited speaker: Tamara von Glehn Polynomial models of type theory 10:00 Maaike Zwart and Dan Marsden Some No-Go Theorems for Distributive Laws (extended abstract) 10:30 Coffee 11:00 Jeremy Pope Formalizing Constructive Quantifier Elimination in Agda 11:45 Exequiel Rivas Relating Idioms, Arrows and Monads from Monoidal Adjunctions 12:30 Lunch 14:00 Invited Speaker: Didier Remy Ornamentation put into practice in ML 15:00 Jeremy Gibbons and Guillaume Boisseau Profunctor Optics and the Yoneda Lemma 15:30 Coffee 16:00 Jules Hedges Backward induction for repeated games 16:45 Conor McBride Everybody's Got To Be Somewhere Program Committee: ================== Andreas Abel - Chalmers, Sweden Danel Ahman - INRIA Paris, France Robert Atkey - University of Strathclyde, UK (co-chair) Jeremy Gibbons - University of Oxford, UK Jennifer Hackett - University of Nottingham, UK Mauro Jaskelioff - Universidad Nacional de Rosario, Argentina Shin-ya Katsumata - National Institute of Informatics, Japan Sam Lindley - University of Edinburgh, UK (co-chair) Clare Martin - Oxford Brookes University, UK Shin-Cheng Mu - Academia Sinica, Taiwan Valeria de Paiva - Nuance Communications, US Alexandra Silva - University College London, UK [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

** Call for participation ** HOR 18 - 9th Workshop on Higher Order Rewriting, Oxford, 7 July, 2018
by Stefano Guerrini 04 Jun '18

04 Jun '18

---------------------------------------------------------------------- ---------------------------------------------------------------------- ** ** HOR 18 ** 9th Workshop on Higher-Order Rewriting ** ** http://lipn.univ-paris13.fr/HOR18 ** ---------------------------------------------------------------------- ** ** International Workshop affiliated with FSCD at FLOC 2018 ** http://www.cs.le.ac.uk/events/fscd2018 ** http://floc2018.org ** ** Oxford, 7 July, 2018 ** ** ** With a special session in honour of Kris Rose ** ** ---------------------------------------------------------------------- ** ** Call for participation ** Early registration deadline: ** 6 June ** ** ** Registration page ** http://www.floc2018.org/register/ ** ---------------------------------------------------------------------- ** ** **** Program **** ** https://easychair.org/smart-program/FLoC2018/HOR-program.html ** ---------------------------------------------------------------------- ---------------------------------------------------------------------- * Overview HOR is a forum to present work concerning all aspects of higher-order rewriting. HOR aims to provide an informal and friendly setting to discuss recent work and work in progress concerning higher-order rewriting, broadly construed. This includes rewriting systems that have functional variables or bound variables, the lambda-calculus and combinatory logic being paradigmatic examples. * Topics The following is a non-exhaustive list of topics for the workshop: - Applications: proof checking, theorem proving, generic programming, declarative programming, program transformation. - Foundations: pattern matching, unification, strategies, narrowing, termination, syntactic properties, type theory. - Frameworks: term rewriting, conditional rewriting, graph rewriting, net rewriting, comparisons of different frameworks. - Implementation: graphs, nets, abstract machines, explicit substitution, rewriting tools, compilation techniques. - Semantics: operational semantics, denotational semantics, separability, higher-order abstract syntax. ---------------------------------------------------------------------- ** Special session in honour of Kris Rose ---------------------------------------------------------------------- Kristopher H. (Kris) Rose has been an active member of the HOR community. He contributed to almost all the editions of HOR and he served as PC chair of the 7th edition (Vienna 2014). The next one will be the first edition without Kris, and a special session will be dedicated to honour him: to thank him for his continuous support to HOR and to acknowledge his key role in the development of explicit substitutions. If you would like to give a short address in his memory or your submission his related to Kris work, please contact the PC chair Stefano Guerrini (mailto:stefano.guerrini@univ-paris13.fr) ---------------------------------------------------------------------- ** Submission Guidelines ---------------------------------------------------------------------- To give a presentation at the workshop, submit an extended abstract (between 2 to 5 pages} via Easychair https://easychair.org/conferences/?conf=hor18 HOR is a platform for discussing open questions, ongoing research, and new perspectives, as well as new results. Extended abstracts describing work in progress, preliminary results, research projects, or problems in higher-order rewriting are very welcome. The workshop has informal, electronic proceedings that will be included in the FLoC 2018 electronic proceedings. Submission is via Easychair at https://easychair.org/conferences/?conf=hor18 For questions regarding submission, please contact the PC chair Stefano Guerrini (mailto:stefano.guerrini@univ-paris13.fr) ---------------------------------------------------------------------- ** Important dates ---------------------------------------------------------------------- * Submission deadline: 15 April, 2017 * Notification: 22 May, 2017 * Final version: 28 May, 2017 ---------------------------------------------------------------------- ** Committees ---------------------------------------------------------------------- ** Program Committee ---------------------------------------------------------------------- * Sandra Alves (University of Porto, Portugal) * Zena Ariola (University of Oregon, Oregon, USA) * Eduardo Bonelli (Stevens Institute of Technology, New Jersey, USA) * Jörg Endrullis (Vrije Universiteit Amsterdam, The Netherlands) * Stefano Guerrini, chair (Paris 13 University, France) * Benedetto Intrigila (Tor Vergata University, Rome, Italy) * Paula Severi (University of Leicester, UK) * Femke Van Raamsdonk (Vrije Universiteit Amsterdam, The Netherlands) ** Steering Committee ---------------------------------------------------------------------- * Delia Kesner (IRIF, Univ. Paris Diderot) * Femke Van Raamsdonk (Vrije Universiteit Amsterdam, The Netherlands) ---------------------------------------------------------------------- ** Invited Speakers ---------------------------------------------------------------------- * Naoki Kobayashi (The University of Tokyo) * Cynthia Kop (Radboud University Nijmegen) * Pierre Vial (CNRS - INRIA Bretagne, Nantes) ---------------------------------------------------------------------- ** Contact ---------------------------------------------------------------------- All questions about submissions should be emailed to Stefano Guerrini (mailto:stefano.guerrini@univ-paris13.fr) ---------------------------------------------------------------------- ** Supporting Organisations ---------------------------------------------------------------------- LIPN, Université Paris 13, Sorbonne Paris Cité ===================================== Stefano Guerrini Institut Galilée, Université Paris 13, Sorbonne Paris Cité Laboratoire d'Informatique de Paris-Nord (LIPN), CNRS (UMR 7030) stefano.guerrini(a)univ-paris13.fr [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

1 0

Vera Trnkova
by Jirí Adámek 04 Jun '18

04 Jun '18

It is with great sadness that I inform you that last Sunday Vera Trnkova has passed away at the age of 84 years. In the last couple of years she suffered from a disease that made her life very difficult, so that she could only leave her appartment in a wheelchair. This is a great loss to the category theory community: Vera was an incredibly enthusiastic and gifted researcher, and her seminars, in which she made it possible for students from their early years to participate at topical research, were a great inspiration to the participants. She published a monograph, coauthored by Ales Pultr, on embeddings of categories, which was one of her life-long topics. And another one, coauthored by me, on the categorical theory of automata. In a series of more than 160 research articles she combined category theory with general topology, theoretical computer science and combinatorics. Another life-long topic of Vera's was the theory of set functors which she and her pupils developed in a substantial series of papers. That theory found applications in diverse areas of mathematics. Vera was also a dear friend, whose personality influenced a number of her colleagues and students. She will be missed by many of us. Jiri Adamek [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

2 1

Point-free affine real line?
by Steve Vickers 01 Jun '18

01 Jun '18

Algebraic geometry defines the affine line over a field k as an affine scheme, the spectrum of k[X]. It includes a copy of k, each element a being present as the irreducible polynomial X-a, with local ring the ring of fractions got by inverting polynomials f(X) such that f(a) is non-zero. You can carry this out for the real line R, but it is very much R as a set, and the copy of R in the underlying space of the spectrum has the discrete topology. Does algebraic geometry provide an analogous construction that could lead to the point-free R? Can the locally ringed space be topologized (point-free) so that the copy of R has its usual topology? I've run into various problems. 1. It is not obvious to me that R[X] exists point-free. By that I mean that, without presupposing a set R[X], or using non-geometric constructions, I can't see how to define a geometric theory whose models are the polynomials. The problem comes with trying to pin down the requirement that all but finitely many of the coefficients of a polynomial must be zero. You cannot continuously define the degree of a polynomial, because the function R -> N, a |-> degree(aX + 1), is not continuous. That suggests the construction as Spec(R[X]) might have to be adjusted. Is there still some locally ringed space that does the trick? 2. The "structure sheaf" cannot be a sheaf. We hope its fibres are point-free local rings, but, whatever they are, they must be R-algebras and so cannot have the discrete topology. The space is locally ringed by some bundle other than a sheaf (local homeomorphism). 3. The usual local rings, got as rings of fractions as described above, may be problematic point-free in the same way as R[X] is. I don't know what would do instead. The power series ring R[[X]]? (At least as fibre over 0.) It does have the property of inverting those polynomials f for which f(0) is non-zero. And it can be defined point-free, as R^N. (However, the finitely presented approximations R[X|X^n = 0] happily exist point-free.) Thanks for any references you can provide, Steve. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]

4 3