McGill Logic, Category Theory, and Computation Seminar Note the new seminar timeslot! Tuesday, 2 February 2016 4:00 - 5:00 M. Barr (McGill) Introduction to *-Autonomous categories [Abstract on webpage] Tuesday, 9 February 2016 4:00 - 5:00 M. Barr (McGill) Introduction to *-Autonomous categories, continued Abstract: I will mention one example I didn't get to yesterday: two equivalent categories of locally convex topological vector spaces. The dualizing object is the topological field C (you could just look at real spaces and use R and get the same results). The first category is the weakly topologized spaces--they have the weak topology for their continuous linear functionals. The second is known as the Mackey spaces, but like the other examples have the strongest possible topology for their continuous linear functionals. Then I will describe the "And then a miracle happened" of the Chu and chu constructions that were based on Mackey's "pairs". Anyone interested in more detail on last week's introduction should look at http://www.math.mcgill.ca/barr/papers/#dsac particularly these two papers: Topological *-autonomous categories (TAC 2006) On duality of topological abelian groups (unpublished note) Some of the other papers in that list might be interesting, but those are the most relevant to what I said on Feb 2nd. Tuesday, 16 February 2016 4:00 - 5:00 M. Barr (McGill) Introduction to *-Autonomous categories, continued Abstract: I will finally get to some of the hard work and show, if time permits, the following two results: 1. Assuming that V is the subobject and product closure of a very nice category S of topological objects and that S contains a very nice injective K, then K is also injective in V. 2. The inclusion of the weak objects in V has a left adjoint and the inclusion of the strong objects has a right adjoint. Tuesday, 23 February 2016 4:00 - 5:00 M. Barr (McGill) Introduction to *-Autonomous categories, continued Abstract: Next time, I will finish proving things about sigma and tau; in particular that tau is left adjoint to sigma. They will be used to show that the inclusions of the categories of weak, resp. strong, objects has a left, resp. right, adjoint and then use generalities on adjoints to show that they are equivalent categories. In future lecture(s), at least one and at most two, I will show that the chu category is equivalent to the category of weak objects, and therefore to the category of strong ones. Since the chu category is *-autonomous, so are they. Then I will discuss examples. One is groups. The others are actually all examples of one rather general situation. Let K be a spherically complete field (this was new to me, see: https://en.wikipedia.org/wiki/Spherically_complete_field), which includes all locally compact fields, then there are *-autonomous categories starting with the normed K-spaces. This includes the case that K is discrete. Tuesday, 15 March 2016 4:00 - 5:00 Brigitte Pientka (McGill) Mechanizing Meta-Theory in Beluga Abstract Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. In this talk, I will survey the proof environment Beluga. To specify formal systems and represent derivations within them, Beluga provides a sophisticated infrastructure based on the logical framework LF; in particular, its infrastructure not only supports modelling binders via binders in LF, but extends and generalizes LF with first-class contexts to abstract over a set of assumptions, contextual objects to model derivations that depend on assumptions, and first-class simultaneous substitutions to relate contexts. These extensions allow us to directly support key and common concepts that frequently arise when describing formal systems and derivations within them. To reason about formal systems, Beluga provides a dependently typed functional language for implementing inductive proofs about derivations as recursive functions on contextual objects following the Curry-Howard isomorphism. Recently, the Beluga system has also been extended with a totality checker which guarantees that recursive programs are well-founded and correspond to inductive proofs and an interactive program development environment to support incremental proof / program construction. Taken together these extensions enable direct and compact mechanizations. To demonstrate Beluga's strength, we develop a weak normalization proof using logical relations. This talk will provide an overview and background of our work. Tuesday, 22 March 2016 4:00 - 5:00 Florence Clerc (McGill) The dual view of Markov Processes I Abstract This is the first of two talks on a dualized view of Markov processes. The first part will describe how to view a probabilistic transition system as a transformer of functions rather than as a transformer of probability distributions. A Markov process is normally viewed as a Markov kernel i.e. a map from S x S ? [0,1] where S is a state space and S is a s-algebra on S. These Markov kernels are morphisms in the Kleisli category of the Giry monad. In recent work by Chaput, Danos, Panangaden and Plotkin, Markov processes were reinterpreted as linear maps on the space of positive L1 functions on S. This is analogous to taking the predicate transformer view of Markov processes. A number of dualities and isomorphisms emerge in this picture. Most interestingly conditional expectation can be understood functorially. In the second part (by Panangaden) the theory of bisimulation and approximation will be presented from this dualized viewpoint. Tuesday, 29 March 2016 4:00 - 5:00 Prakash Panangaden (McGill) The dual view of Markov Processes II I will describe the dual view of Markov processes as expectation value transformers. I will then define a category of "abstract" Markov processes and show how approximation and bisimulation both co-exist and are on the same footing. Tuesday, 5 April 2016 4:00 - 5:00 Prakash Panangaden (McGill) The dual view of Markov Processes III Abstract I will discuss finite approximation and show how an abstract Markov process can be reconstructed as the projective limit of its finite approximants. I will relate this to minimal realization for Markov processes. Tuesday, 12 April 2016 4:00 - 5:00 Michel Vaquié (Toulouse) System of points in saturated dg-categories Abstract In this work we consider the question of realizing triangulated dg-categories by derived categories of algebraic varieties. For this, we introduce the notion of "system of points" in saturated dg-categories. We show that given such a system on a dg-category T, we can construct an algebraic space M, of finite type, smooth and separated, together with a dg-functor from T to a certain twisted dg-category of sheaves on M. We prove that this functor is furthermore an equivalence if and only if M is proper. All along this work we study t-strutcures on algebraic families of objects in T, which might be of independant interest. Ref: http://arxiv.org/abs/1504.07748 (Joint work with Bertrand Toen) Schedule of talks for 2016 - 2017 20 September 2016 2:30 - 3:30 M. Makkai (McGill) Higher dimensional categories from a logician's point view [Abstract on web] 27 September 2016 2:30 - 3:30 M. Barr (McGill) Is the category of finite distributive sup semilattices compact *-autonomous? Abstract It is *-autonomous, but not compact. 4 October 2016 2:30 - 3:30 M. Makkai (McGill) Higher dimensional categories from a logician's point view II [This continues the talk of 20 Sept] 18 October 2016 2:30 - 3:30 M. Makkai (McGill) A brief survey of what higher categories do in logic and mathematics 25 October 2016 2:30 - 3:30 M. Makkai (McGill) A brief survey of what higher categories do in logic and mathematics II 1 November 2016 2:30 - 3:30 André Joyal (UQAM) A general theory of algebras and coalgebras [Abstract on webpage] Friday, 4 November 2016 in BH1B23 3:30 - 4:40 Danny Rorabaugh (Queen's U) Bridging Logic and Constraint Satisfaction with Relational Structures and Filters [Abstract on webpage] 8 November 2016 2:30 - 3:30 Amit Sharma (McGill) Symmetric monoidal quasicategories [Abstract on webpage] 15 November 2016 2:30 - 3:30 Eduardo Dubuc (UBA) On the notion of flat 2-functors [Abstract on webpage] Thursday, 17 November 2016 at UdeM (address below) 2:00 - 4:00 M. Makkai (McGill) In defense of Bourbaki's structuralism [Abstract on webpage] Note: This is not part of this seminar's activities, but may be of interest to our regular participants. Location: The talk will be held in the Dept of Philosophy, 2910 Edouard-Montpetit, Room 422. 6 December 2016 2:30 - 3:30 M. Barr (McGill) The regular category embedding theorem [Abstract on webpage] =================================================== PLACE: BURNSIDE HALL 920, McGILL UNIVERSITY (unless otherwise indicated) =================================================== (Any comments, suggestions to rags@math.mcgill.ca) Seminar listings are available here: http://www.math.mcgill.ca/triples The latest revised details about talks and times are to be found there.