## Theoretical computer science seminar
Add to your list(s)
Send you e-mail reminders
Further detail
Seminar series in theoretical computer science 4 upcoming talks and 538 talks in the archive: show all (slow!). ## The Fine-Grained Complexity of Pattern Counting ProblemsMarc Roth (University of Oxford). LG23, SoCS and Zoom (see abstract for link). Friday 27 May 2022, 14:00-15:00 ## From intuitionistic justification logic to explicit modal type theory with diamondSonia Marin (University of Birmingham). LG23, SoCS and Zoom (see abstract for link). Thursday 26 May 2022, 14:00-15:00 ## Learning algorithms versus automatability of Frege systemsJán Pich. LG23, SoCS and Zoom (see abstract for link). Thursday 19 May 2022, 14:00-15:00 ## Kripke Semantics for Intuitionistic Łukasiewicz LogicPaulo Oliva (Queen Mary, University of London). LG23, SoCS and Zoom (see abstract for link). Friday 13 May 2022, 14:00-15:00 ## Model Theory ex Proof-searchAlexander Gheorghiu (University College London). LG23, SoCS and Zoom (see abstract for link). Friday 06 May 2022, 14:00-15:00 ## Apartness in constructive domain theory: part IITom de Jong (Birmingham). LG23, SoCS and Zoom (see abstract for link). Thursday 05 May 2022, 14:00-15:00 ## Model Counting meets F0 EstimationKuldeep Meel (National University of Singapore). LG23, SoCS and Zoom (see abstract for link). Friday 29 April 2022, 14:00-15:00 ## Apartness in constructive domain theoryTom de Jong (University of Birmingham). LG23, SoCS and Zoom (see abstract for link). Thursday 28 April 2022, 14:00-15:00 ## Zigzag games, alternating infinite word automata and linear Monadic-Second order logicPierre Pradic (University of Swansea). LG23, SoCS and Zoom (see abstract for link). Friday 08 April 2022, 14:00-15:00 ## Regular string-to-string function in the linear λ-calculusPierre Pradic (University of Swansea). LG23, SoCS and Zoom (see abstract for link). Thursday 07 April 2022, 14:00-15:00 ## Implicit automata in typed λ-calculiLê Thành Dũng Nguyễn (École Polytechnique). LG23, SoCS and Zoom (see abstract for link). Friday 01 April 2022, 14:00-15:00 ## The coherence space semantics of purely linear system F is finite and effectiveLê Thành Dũng Nguyễn (Tito). LG23, SoCS and Zoom (see abstract for link). Thursday 31 March 2022, 14:00-15:00 ## Transducers of polynomial growthMikołaj Bojańczyk (University of Warsaw). LG23, SoCS and Zoom (see abstract for link). Friday 25 March 2022, 14:00-15:00 ## Semantic evaluation in the simply typed λ-calculus: implicit complexity and normalizationLê Thành Dũng Nguyễn (Tito). LG23, SoCS and Zoom (see abstract for link). Thursday 24 March 2022, 14:00-15:00 ## Recent results and open questions in applied proof theoryTom Powell (University of Bath). LG23, SoCS and Zoom (see abstract for link). Friday 18 March 2022, 14:00-15:00 ## Specker sequences and their relevance to Proof MiningMorenikeji Neri. LG23, SoCS and Zoom (see abstract for link). Thursday 17 March 2022, 14:00-15:00 ## The Berry Order (ideas from 1980s stable domain theory)Paul Taylor (University of Birmingham). LG23, SoCS and Zoom (see abstract for link). Friday 11 March 2022, 14:00-15:00 ## Teaching complexity theory without machines, some reflections: part IIAnupam Das, University of Birmingham. LG23, SoCS and Zoom (see abstract for link). Thursday 10 March 2022, 14:00-15:00 ## Cyclic Proofs, Hypersequents, and Transitive Closure LogicMarianna Girlando (University of Birmingham). LG23, SoCS and Zoom (see abstract for link). Friday 25 February 2022, 14:00-15:00 ## Teaching complexity theory without machines, some reflectionsAnupam Das, University of Birmingham. LG23, SoCS and Zoom (see abstract for link). Thursday 24 February 2022, 14:00-15:00 ## Seemingly impossible programs and proofsMartin Escardo, Theory Group, School of Computer Science, University of Birmingham. LG23, SoCS and Zoom (see abstract for link). Friday 11 February 2022, 14:00-15:00 ## Comprehension bicategoriesNiels van der Weide, University of Birmingham. LG23, SoCS and Zoom (see abstract for link). Friday 10 December 2021, 14:00-15:00 ## Constructing fully-abstract models of effectful λ-calculiPhilip Saville, University of Oxford. LG23, SoCS and Zoom (see abstract for link). Friday 03 December 2021, 14:00-15:00 ## Synthetic fibered (∞,1)-category theoryJonathan Weinberger (University of Birmingham). LG23, SoCS and Zoom (see abstract for link). Friday 26 November 2021, 14:00-15:00 ## Confluence with basic effectsWillem Heijltjes (University of Bath). LG23, SoCS and Zoom (see abstract for link). Friday 19 November 2021, 14:00-15:00 ## From axioms to synthetic inference rules via focusingSonia Marin (University of Birmingham). LG23, SoCS and Zoom (see abstract for link). Friday 12 November 2021, 14:00-15:00 ## Categorifying Intersection TypesFederico Olimpieri (University of Leeds). LG23, SoCS and Zoom (see abstract for link). Friday 29 October 2021, 14:00-15:00 ## A Type Theory for Strictly Associative Infinity CategoriesAlex Rice. LG23, SoCS and Zoom (see abstract for link). Friday 22 October 2021, 14:00-15:00 ## Part III: Some musings on circular proofs and the metamathematical approach to proof mining and higher-order computabilityAnupam Das, University of Birmingham. LG23, SoCS and Zoom (see abstract for link). Thursday 21 October 2021, 13:00-14:00 ## Solving Verification Questions using Machine LearningMirco Giacobbe, University of Birmingham. LG23, SoCS and Zoom (see abstract for link). Friday 15 October 2021, 14:00-15:00 ## Part II: Some musings on circular proofs and the metamathematical approach to proof mining and higher-order computabilityAnupam Das, University of Birmingham. Thursday 14 October 2021, 13:00-14:00 ## Some musings on circular proofs and the metamathematical approach to proof mining and higher-order computabilityJoin the Zoom meeting below, or join in person in the LG seminar room. Dr Anupam Das (University of Birmingham). https://bham-ac-uk.zoom.us/j/83640520145?pwd=RmJ1a1ZvamNEVG1Sa0ZlN3plaTFHQT09. Friday 08 October 2021, 14:00-15:00 ## Types are Internal oo-Groupoidshttps://bham-ac-uk.zoom.us/j/83662748860?pwd=dTBRV1JCUEgxQXV1cXpjV3pDaGttUT09 Eric Finster, School of Computer Science, University of Birmingham. LG23, SoCS and Zoom (see abstract for link). Friday 24 September 2021, 14:00-15:00 ## The Strange Career of Interpolation and DefinabilityMichael Benedikt, University of Oxford. LG23, SoCS and Zoom (see abstract for link). Wednesday 08 September 2021, 14:00-15:00 ## Logic beyond formulas: a proof system on graphsMatteo Acclavio, Université du Luxembourg. Friday 03 September 2021, 14:45-15:30 ## Canonical proof-objects for coinductive programmingAbhishek De, Institut de Recherche en Informatique Fondamentale. Friday 03 September 2021, 14:00-14:45 ## Hierarchical string diagram for closed monoidal categoriesDan Ghica (Computer Science). Friday 09 July 2021, 14:00-15:00 ## Hierarchical string diagrams for closed monoidal categoriesDan Ghica (Computer Science). https://bham-ac-uk.zoom.us/j/87347393966?pwd=SndiVlNCZStOSER0c0NKNUoxWkVZUT09. Tuesday 06 July 2021, 14:00-15:00 ## Automatic differentiation in string diagramsMario Alvarez Picallo, Huawei Research. https://bham-ac-uk.zoom.us/j/4040590387?pwd=dlJpN0tyUVJQQWxyUzc3SisvcHJtUT09. Friday 02 July 2021, 14:00-15:00 ## Proof complexity of positive branching programsAvgerinos Delkos. Via Zoom (see link in abstract). Friday 25 June 2021, 14:00-15:00 ## Adelic Geometry via Topos Theory (note change in time!)Ming Ng. https://bham-ac-uk.zoom.us/j/4040590387?pwd=dlJpN0tyUVJQQWxyUzc3SisvcHJtUT09. Thursday 24 June 2021, 16:00-17:00 ## New minimal linear inferences in Boolean logic independent of switch and medialAlex Rice (University of Cambridge). https://bham-ac-uk.zoom.us/j/4040590387?pwd=dlJpN0tyUVJQQWxyUzc3SisvcHJtUT09. Friday 11 June 2021, 13:00-14:00 ## The smash product of monoidal theoriesAmar Hadzihasanovic. https://bham-ac-uk.zoom.us/j/82118141256?pwd=TWNqRXpFclZ6RG1lNmQ4VTVGTXZFQT09. Friday 30 April 2021, 14:00-15:00 ## Environments & CPS translations, a well-typed storyEtienne Miquey, ENS Lyon. https://bham-ac-uk.zoom.us/j/81751920321?pwd=Vkk4NEtqNWl1TjhSeC9IN281KytnQT09. Friday 19 March 2021, 14:00-15:00 ## On the proof theory of conditional logicsMarianna Girlando. University of Birmingham.. Zoom link at the bottom of the abstract. Friday 12 March 2021, 14:00-15:00 ## Reparametrizing gradient descentDavid Sprunger, University of Birmingham. Zoom link at the bottom of the abstract. Friday 12 February 2021, 16:00-17:00 ## Domain Theory in Constructive and Predicative Univalent FoundationsThis is a Lab Lunch Talk. Notice that the Zoom link has changed. We meet at 13:45 to socialize and the talk starts at 14:00. Tom de Jong, School of Computer Science, University of Birmingham. Zoom link at the bottom of the abstract. Thursday 14 January 2021, 13:45-15:00 ## Circularly typed programs and their abstraction complexityDr Anupam Das (University of Birmingham). https://bham-ac-uk.zoom.us/my/lablunch. Thursday 17 December 2020, 13:55-15:00 ## A minimal cyclic formal framework for coinductionLiron Cohen, Ben-Gurion University. https://bham-ac-uk.zoom.us/j/81751920321?pwd=Vkk4NEtqNWl1TjhSeC9IN281KytnQT09. Friday 11 December 2020, 13:00-14:00 ## Combining cyclic proofs and implicit complexityGianluca Curzi (University of Birmingham). https://bham-ac-uk.zoom.us/my/lablunch. Thursday 10 December 2020, 13:55-15:00 ## The Graphical Language of Symmetric Traced Monoidal CategoriesGeorge Kaye (University of Birmingham). https://bham-ac-uk.zoom.us/my/lablunch. Thursday 03 December 2020, 13:55-15:00 ## Broad Infinity and Generation PrinciplesVirtual Lab Lunch - Passcode: 217 Paul Levy (University of Birmingham). https://bham-ac-uk.zoom.us/my/lablunch. Thursday 26 November 2020, 13:55-15:00 ## Arithmetic universes: Home of free algebrasGiven as invited contribution to the Erik Palmgren memorial conference, 19-21 Nov 2020 Steve Vickers, CS Theory Group Birmingham . Friday 20 November 2020, 14:10-15:10 ## Extracting nested relational queries from implicit definitionsPierre Pradic (University of Oxford). https://bham-ac-uk.zoom.us/j/4040590387?pwd=dlJpN0tyUVJQQWxyUzc3SisvcHJtUT09. Wednesday 04 November 2020, 13:45-15:30 ## On program equivalence in the probabilistic lambda calculusGianluca Curzi (University of Birmingham). https://bham-ac-uk.zoom.us/j/4040590387?pwd=dlJpN0tyUVJQQWxyUzc3SisvcHJtUT09. Friday 23 October 2020, 13:45-15:30 ## Lovász' Theorem and Comonads in Finite Model TheoryThe talk is at 2pm. We start at 1:50 for socializing with the speaker. Tomáš Jakl, Cambridge University, https://www.cl.cam.ac.uk/~tj330/. https://bham-ac-uk.zoom.us/j/91939191081?pwd=THdqTXRsRWl1aDl5VDhTN2thckt6UT09. Friday 25 September 2020, 13:50-15:00 ## Whisker-based biased composition in infinity categoriesAlex is leaving the School sadly, so this will be his last talk as an internal speaker! Alex Rice (University of Birmingham). https://bham-ac-uk.zoom.us/my/lablunch. Thursday 24 September 2020, 13:55-15:00 ## Pointfree Construction of Positive Real ExponentiationMing Ng (University of Birmingham). https://bham-ac-uk.zoom.us/my/lablunch. Thursday 27 August 2020, 13:55-15:00 ## Formal topology and GRD-systemsDr Steve Vickers (School of Computer Science, University of Birmingham). https://bham-ac-uk.zoom.us/my/lablunch. Thursday 13 August 2020, 13:55-15:00 ## Formal topology and GRD-systemsDr Steve Vickers (School of Computer Science, University of Birmingham). https://bham-ac-uk.zoom.us/my/lablunch. Thursday 13 August 2020, 13:55-15:00 ## Formal Topology in Univalent FoundationsAyberk is a new Ph.D. student with Martín Escardó. Ayberk Tosun (University of Birmingham). https://bham-ac-uk.zoom.us/my/lablunch. Thursday 23 July 2020, 13:00-14:00 ## Intutions on domain theory and geometryMartin Escardo, Theory Lab, School of Computer Science, University of Birmingham. https://bham-ac-uk.zoom.us/j/94667894207?pwd=ZlhSaVlzZUljVHJzMzJpd0MxbExUZz09. Friday 26 June 2020, 16:00-17:00 ## Quantitative Tauberian theoremsTom Powell, University of Bath. https://bham-ac-uk.zoom.us/j/96981634161?pwd=TmNFdGFBbzdqcjV0SG43a3BjSWM5UT09. Friday 12 June 2020, 14:00-15:00 ## An Authoritarian Approach to PresheavesPierre-Marie Pédrot (INRIA). https://us02web.zoom.us/j/82603907326. Friday 05 June 2020, 14:00-15:00 ## Formalising the Escardó-Simpson Interval Object in UTTPreceded by a coffee break at 13:30 Todd Waugh Ambridge (University of Birmingham). https://bham-ac-uk.zoom.us/my/lablunch. Thursday 04 June 2020, 14:00-15:00 ## Elementary doctrines as coalgebrasJacopo Emmenegger, University of Birmingham. https://us02web.zoom.us/j/82603907326. Friday 29 May 2020, 16:00-17:00 ## Bifibrations of Polycategories and Classical Linear LogicNOTE the earlier time of 13:30 Nicolas Blanco (University of Birmingham). Zoom. Thursday 28 May 2020, 13:25-14:30 ## Synthetic probability theoryAlex Simpson, University of Ljubljana. https://us02web.zoom.us/j/82603907326. Friday 22 May 2020, 14:00-15:00 ## A Theory of Particular SetsPreceded by a coffee break at 13:30 Paul Levy (University of Birmingham). https://us02web.zoom.us/j/82603907326?pwd=dXlBdmh0RnRZTDc0Zk1pQXhndWI4Zz09. Thursday 21 May 2020, 13:55-15:00 ## Formalising mathematics in a theorem proverKevin Buzzard, Imperial College. https://us02web.zoom.us/j/85861947051?pwd=OXk3OW96Z3k5ZHZlOFlpRVdyS2dtZz09. Friday 15 May 2020, 14:00-15:00 ## The ring of adeles from a homotopical viewpointPreceded by a coffee break at 13:30 Scott Balchin (University of Warwick). Zoom. Thursday 14 May 2020, 13:55-15:00 ## Near-Optimal Complexity Bounds for Fragments of the Skolem ProblemNikhil Balaji, University of Oxford. Zoom. Friday 08 May 2020, 14:00-15:00 ## Booij’s locators point-freehttps://us02web.zoom.us/j/82603907326?pwd=dXlBdmh0RnRZTDc0Zk1pQXhndWI4Zz09 Dr Steve Vickers (School of Computer Science, University of Birmingham). Zoom. Thursday 07 May 2020, 14:00-15:00 ## Identity, indiscernibility, and univalence: a higher structure identity principleMike Shulman, University of San Diego. Zoom. Friday 01 May 2020, 20:30-21:30 ## On linear rewriting systems for Boolean logic and some applications to proof theory (2)https://us04web.zoom.us/j/7744570352 Dr Anupam Das (University of Birmingham). Zoom. Thursday 30 April 2020, 14:00-15:00 ## Trace Theory for Probability and NondeterminismAna Sokolova, University of Salzburg. Zoom. Friday 24 April 2020, 11:00-12:00 ## Introduction to the ZX-calculus (2)https://us04web.zoom.us/j/7744570352 Miriam Backens (School of Computer Science, University of Birmingham). Zoom. Thursday 23 April 2020, 14:00-15:00 ## Introduction to the ZX-calculushttps://us04web.zoom.us/j/498274768 https://us04web.zoom.us/j/305829441 Miriam Backens (School of Computer Science, University of Birmingham). Zoom. Thursday 09 April 2020, 11:00-12:00 ## On linear rewriting systems for Boolean logic and some applications to proof theoryDr Anupam Das (University of Birmingham). Zoom. Thursday 02 April 2020, 12:00-13:00 ## Analysis in Univalent Type TheoryThis will be a Virtual Lab Lunch: https://zoom.us/j/615775681 Auke Booij (UoB). Zoom. Thursday 26 March 2020, 12:00-13:00 ## Coinductive Invertibility in Higher Categorieshttps://meet.google.com/ecc-quzw-qyq Alex Rice (University of Birmingham). Thursday 19 March 2020, 12:00-13:00 ## ZX-calculus and its applicationsQuanlong Wang, Oxford. Computer Science, The Sloman Lounge (UG). Friday 06 March 2020, 11:00-12:00 ## From Brouwer's Thesis to the Fan FunctionalUlrich Berger (Swansea University). Computer Science, The Sloman Lounge (UG). Friday 21 February 2020, 11:00-12:00 ## Consistency of circuit lower bounds with bounded theoriesIgor Carboni Oliveira (Warwick University). Computer Science, The Sloman Lounge (UG). Friday 14 February 2020, 11:00-12:00 ## Gödel's incompleteness theorem using arithmetic universeschange of venue Alexander Gietelink Oldenziel (Amsterdam). Friday 07 February 2020, 11:00-12:00 ## The Cantor-Schröder-Bernstein Theorem for ∞-groupoidsMartin Escardo (School of Computer Science). Thursday 06 February 2020, 12:00-13:00 ## Induction for CyclesNicolai Kraus (University of Birmingham). Computer Science, The Sloman Lounge (UG). Friday 31 January 2020, 11:00-12:00 ## Revisiting the relation between subspaces and sublocalesAnna Laura Suarez (University of Birmingham). Thursday 23 January 2020, 12:00-13:00 ## On the complexity of linear arithmetic theories over the integersDmitry Chistikov, University of Warwick. Computer Science, The Sloman Lounge (UG). Friday 17 January 2020, 11:00-12:00 ## Constructing Infinitary Quotient-Inductive TypesAndy Pitts (University of Cambridge). Computer Science, The Sloman Lounge (UG). Friday 10 January 2020, 11:00-12:00 ## Well founded coalgebras and recursionPaul Taylor (Computer Science, University of Birmingham, honorary). Thursday 12 December 2019, 12:00-13:00 ## Proof complexity through the lens of the pigeon hole principle IIDr Anupam Das (University of Birmingham). Thursday 05 December 2019, 12:00-13:00 ## String diagrams for cartesian bicategories and their Karoubi envelopes - and entailment systemsDr Steve Vickers (School of Computer Science, University of Birmingham). Thursday 21 November 2019, 12:00-13:00 ## Algorithms and Complexity through the eyes of Vertex Cover (Part 2)Part 2 of last week's talk Rajesh Chitnis (University of Birmingham). Thursday 07 November 2019, 12:00-13:00 ## Taylor expansion in linear logic is invertible: A completeness resultDaniel de Carvalho, Innopolis University. Computer Science, The Sloman Lounge (UG). Friday 01 November 2019, 11:00-12:00 ## Algorithms and Complexity through the eyes of Vertex CoverRajesh Chitnis (University of Birmingham). Thursday 31 October 2019, 12:00-13:00 ## Nested proof systems for modal logics (and beyond)Sonia Marin, UCL. Computer Science, The Sloman Lounge (UG). Friday 25 October 2019, 11:00-12:00 ## Internal higher-categorical models of dependent type theoryPlease contact Todd if you wish to give a talk this term! Nicolai Kraus (University of Birmingham). Thursday 24 October 2019, 12:00-13:00 ## Algorithmic Human Development: What is it and why do we need it now?Note unusual time Professor Abbas Edalat, Imperial College London. Computer Science, The Sloman Lounge (UG). Friday 18 October 2019, 14:00-15:00 ## On the logical complexity of cyclic arithmeticAnupam Das, University of Birmingham. Computer Science, The Sloman Lounge (UG). Friday 11 October 2019, 11:00-12:00 ## A Brouwerian Intuitionistic Type Theory (Part 3)Please contact Todd if you wish to give a talk this term! Vincent Rahli (University of Birmingham). Thursday 10 October 2019, 12:00-13:00 ## Diagram rewriting in double categoriesAntonin Delpeuch, University of Oxford. Computer Science, The Sloman Lounge (UG). Friday 04 October 2019, 11:00-12:00 ## A Brouwerian Intuitionistic Type Theory (Part 2)First talk of the term. Please contact Todd if you wish to give a talk this term! Vincent Rahli (University of Birmingham). Thursday 03 October 2019, 12:00-13:00 ## Transparent synchronous dataflowSteven Cheung, University of Birmingham. Thursday 15 August 2019, 12:00-13:00 ## A Brouwerian Intuitionistic Type TheoryVincent Rahli, CS Theory Group, Birmingham. Thursday 25 July 2019, 12:00-13:00 ## Foundational end-to-end verification of cyber-physical systems: The VeriPhy pipeline and its ApplicationsBrandon Bohrer (Carnegie Mellon). Computer Science, The Sloman Lounge (UG). Friday 19 July 2019, 11:00-12:00 ## Constructive Brouwer Fixed Point TheoremPaul Taylor (Computer Science, University of Birmingham, honorary). Friday 12 July 2019, 11:00-12:00 ## Rudimentary recursionAdrian Mathias. Computer Science, The Sloman Lounge (UG). Friday 21 June 2019, 11:00-12:00 ## A Sound and Complete Logic for Algebraic EffectsCristina Matache (Oxford). Computer Science, The Sloman Lounge (UG). Friday 14 June 2019, 11:00-12:00 ## Geometric morphisms as structure preserving maps and other nice characterisationsChristopher Townsend. Computer Science, The Sloman Lounge (UG). Friday 07 June 2019, 10:30-12:00 ## The coproduct of frames as encoding d-frame structureAnna Laura Suarez, CS Theory Group Birmingham. Thursday 06 June 2019, 12:00-13:00 ## Reasoning about effectful programs and evaluation orderDylan McDermott (Cambridge). Computer Science, The Sloman Lounge (UG). Friday 31 May 2019, 11:00-12:00 ## Reasoning about entailment in natural language data using vectors, density matrices, and category theoryMehrnoosh Sadrzadeh, Queen Mary. Wednesday 29 May 2019, 11:00-12:00 ## Two Sides of the Same Coin: Session Types and Game SemanticsSimon Castellan, Imperial College London. Computer Science, The Sloman Lounge (UG). Friday 24 May 2019, 11:00-12:00 ## Graph Theory and the TransfiniteMichael Rathjen (Leeds). Computer Science, The Sloman Lounge (UG). Friday 17 May 2019, 11:00-12:00 ## Denotational Semantics of Linear Logic with Least and Greatest FixpointsFarzad Jafarrahmani, ENS Cachan. Thursday 09 May 2019, 12:00-13:00 ## Designing an algebraic effect system for OCamlLeo White, Jane Street. Computer Science, The Sloman Lounge (UG). Friday 22 March 2019, 11:00-12:00 ## Operational approaches to the foundations of physicsLucien Hardy, Perimeter Institute. Thursday 14 March 2019, 12:00-13:00 ## Linear Implicative Algebras, a Brouwer-Heyting-Kolmogorov interpretation of linear logicLuc Pellissier, IRIF, Université Paris Diderot. Computer Science, The Sloman Lounge (UG). Friday 08 March 2019, 11:00-12:00 ## The lifting monad in infinity-groupoids, or types in univalent mathematicsNote room 245 this week Martin Escardo, CS Theory Group Birmingham. Thursday 07 March 2019, 12:00-13:00 ## Proof-Carrying PlansEkaterina Komendantskaya, Heriot-Watt University. Computer Science, The Sloman Lounge (UG). Friday 01 March 2019, 11:00-12:00 ## The lifting monad in infinity-groupoids, or types in univalent mathematicsNote changed time and place, theory seminar slot for lab lunch talk Martin Escardo (School of Computer Science). Friday 22 February 2019, 11:00-12:00 ## The Scott model of PCF in UniMathMartin Escardo's talk has been postponed to Friday 22, Sloman Lounge at 11.00 Tom de Jong, Birmingham CS Theory Group. Thursday 21 February 2019, 12:00-13:00 ## Unrestricted Quantification and the Structure of Type TheorySalvatore Florio and Nicholas K Jones, University of Birmingham (Philosophy). Computer Science, The Sloman Lounge (UG). Friday 15 February 2019, 11:00-12:00 ## COMPUTER PROBLEMS POSED BY DESSINS D'ENFANTS THEORYGeorge Shabat, Russian State University for the Humanities and Independent University of Moscow. Monday 11 February 2019, 14:00-15:00 ## Numerically Definite LogicRichard Kaye, University of Birmingham (Mathematics). Computer Science, The Sloman Lounge (UG). Friday 08 February 2019, 11:00-12:00 ## BAGSPACES, (OP)FIBRATIONS, AND COLIMITS OF POINT-FREE GENERALIZED SPACESSteve Vickers, CS Theory Group Birmingham. Thursday 07 February 2019, 12:00-13:00 ## BAGSPACES, (OP)FIBRATIONS, AND COLIMITS OF POINT-FREE GENERALIZED SPACESSteve Vickers, CS Theory Group Birmingham. Thursday 07 February 2019, 12:00-13:00 ## Bagspaces, (op)fibrations, and colimits of point-free generalized spacesNote room 245 Steve Vickers, CS Theory Group Birmingham. Thursday 31 January 2019, 12:00-13:00 ## Strategic Graph Rewriting in PORGY — an interactive modelling frameworkMaria Isabel Fernandez, King's College London. Computer Science, The Sloman Lounge (UG). Friday 25 January 2019, 11:00-12:00 ## Higher Universal Algebra in Type TheoryEric Finster, INRIA, Paris. Thursday 24 January 2019, 12:00-13:00 ## Higher Universal Algebra in Type TheoryEric Finster, INRIA, Paris. Tuesday 22 January 2019, 15:00-16:00 ## Fibrations and opfibrations of generalized point-free spacesSteve Vickers, CS Theory Group Birmingham. Thursday 17 January 2019, 12:00-13:00 ## Towards Coherence for Guarded TracesSergey Goncharov, FAU Erlangen-Nürnberg. Monday 07 January 2019, 11:00-12:00 ## Don't Try This at Home: No-Go Theorems for Distributive LawsDaniel Marsden, University of Oxford. Computer Science, The Sloman Lounge (UG). Friday 14 December 2018, 11:00-12:00 ## Fibrations and opfibrations of toposesSina Hazratpour, CS Theory Group, Birmingham. Thursday 29 November 2018, 12:00-13:00 ## Reflection principles in subsystems of analysisEmanuele Frittaion, University of Leeds. Computer Science, The Sloman Lounge (UG). Friday 23 November 2018, 10:30-11:30 ## A foundation for machine learning from Peirce's Logic of ScienceDan Ghica, CS Theory Group, Birmingham. Thursday 22 November 2018, 12:00-13:00 ## Reverse mathematics of non-deterministic inductive definitionsHajime Ishihara (JAIST). Monday 19 November 2018, 15:00-16:30 ## Polynomials via fibrationsTamara von Glehn, University of Cambridge. Computer Science, The Sloman Lounge (UG). Friday 16 November 2018, 10:30-11:30 ## Beck in control: Algebraic interpretation of a call-by-push-value dialect with control effect(Dan Ghica's advertised talk has been postponed to next week.) Yuning Feng. Thursday 15 November 2018, 12:00-13:00 ## Some Open Problems in Homotopy Type TheoryNicolai Kraus, University of Nottingham. Computer Science, The Sloman Lounge (UG). Friday 09 November 2018, 10:30-11:30 ## Discrete spaces are opfibrant, Stone spaces are fibrant (categorically) - and why it mattersContinued from previous week. Dan Ghica's advised talk will be next week. Steve Vickers, CS Theory Group, Birmingham. Thursday 08 November 2018, 12:00-13:00 ## Quantitative Algebraic ReasoningRadu Mardare, University of Aalborg. Computer Science, The Sloman Lounge (UG). Friday 02 November 2018, 10:30-11:30 ## Discrete spaces are opfibrant, Stone spaces are fibrant (categorically) - and why it mattersPostponed from 25 Oct Steve Vickers, CS Theory Group Birmingham. Thursday 01 November 2018, 12:00-13:00 ## Quasitopoi and universes of propositionsPaolo Capriotti, University of Nottingham. Computer Science, The Sloman Lounge (UG). Friday 26 October 2018, 11:00-12:00 ## Compact ordinals in constructive univalent mathematics(Steve Vickers's advertised talk is postponed to next week) Martin Escardo, CS Theory Group, Birmingham. Thursday 25 October 2018, 12:00-13:00 ## Towards a Formal Theory of Renaming for OCamlReuben Rowe, University of Kent. Computer Science, The Sloman Lounge (UG). Friday 19 October 2018, 10:30-11:30 ## Compact ordinals in constructive univalent mathematicsWe found a room after all! Martin Escardo, CS Theory Group, Birmingham. Thursday 18 October 2018, 12:00-13:00 ## Completing the ZX-calculusMiriam Backens, University of Oxford. Computer Science, The Sloman Lounge (UG). Friday 12 October 2018, 11:00-12:00 ## Formulating categorical concepts using classesContinuation of last week's talk. Paul Levy, CS Theory Group Birmingham. Thursday 11 October 2018, 12:00-13:00 ## Formulating categorical concepts using classesPaul Levy, CS Theory Group Birmingham. Thursday 04 October 2018, 12:00-13:00 ## Hypergraph categories as cospan algebrasBrendan Fong, MIT. Computer Science, The Sloman Lounge (UG). Wednesday 19 September 2018, 14:00-15:00 ## Postponed (Topological structure in single molecular imaging)POSTPONED - new date not fixed yet. Iain Styles, School of Computer Science, UoB. Tuesday 21 August 2018, 13:00-14:00 ## Understanding Girard’s ParadoxThorsten Altenkirch (Nottingham). 217, School of Computer Science. Tuesday 03 July 2018, 13:15-14:15 ## A homotopy type theory for directed homotopy theoryPaige North. Computer Science, The Sloman Lounge (UG). Friday 08 June 2018, 11:00-12:00 ## REBA: A Refinement-Based Architecture for Knowledge Representation and Reasoning in RoboticsNote change of time and room. Mohan Sridharan, SoCS. Tuesday 15 May 2018, 12:00-13:00 ## Magnitude of Metric SpacesSimon Willerton (Maths, Sheffield). Computer Science, The Sloman Lounge (UG). Friday 11 May 2018, 11:00-12:00 ## Future directions for JavaGavin Bierman (Oracle, Cambridge). Computer Science, The Sloman Lounge (UG). Friday 04 May 2018, 11:00-12:00 ## A Unified Perspective of Linear Time Logics using CoalgebrasCorina Cirstea (Southampton). Computer Science, The Sloman Lounge (UG). Friday 27 April 2018, 11:00-12:00 ## Ordinals vs. Cardinals in N? and BeyondSpecial seminar arranged by Aaron Sloman Aviv Keren (Jerusalem). Computer Science, The Sloman Lounge (UG). Wednesday 11 April 2018, 11:00-12:00 ## Physical oracles: Measurement, complexity and cyber-physical systemsEdwin Beggs (Maths, Swansea University). Computer Science, The Sloman Lounge (UG). Friday 23 March 2018, 11:00-12:00 ## (Op)fibrations of toposesRoom changed Sina Hazratpour, CS Theory Group Birmingham. Tuesday 20 March 2018, 13:00-14:00 ## Univalent mathematics - continuedMartin Escardo, CS Theory Group Birmingham. Tuesday 13 March 2018, 13:00-14:00 ## Geometric/AU mathematicsSteve Vickers, CS Theory Group Birmingham. Tuesday 06 March 2018, 13:00-14:00 ## An Algebraic Combinatorial Approach to the Abstract Syntax of Opetopic StructuresMarcelo Fiore (Cambridge). Computer Science, The Sloman Lounge (UG). Friday 02 March 2018, 11:00-12:00 ## Univalent mathematicsNote not usual room Martin Escardo, CS Theory Group Birmingham. Tuesday 27 February 2018, 13:00-14:00 ## Handlers in Scope with AdjunctionsNicholas Wu (Bristol). Computer Science, The Sloman Lounge (UG). Friday 23 February 2018, 11:00-12:00 ## Linear typings as flows on 3-valent graphs (part 3)Noam Zeilberger, CS Theory Group Birmingham. Tuesday 20 February 2018, 13:00-14:00 ## Concurrent Kleene Algebra: free model and completenessAlexandra Silva (UCL). Computer Science, The Sloman Lounge (UG). Friday 16 February 2018, 11:00-12:00 ## The Dialectica models of type theoryroom 217, not Sloman Lounge Sean Moss (Oxford, formerly Cambridge). 217, School of Computer Science. Friday 09 February 2018, 11:00-12:00 ## Linear typings as flows on 3-valent graphsNoam Zeilberger, CS Theory Group Birmingham. Tuesday 06 February 2018, 13:00-14:00 ## The Church-Turing Thesis and denotational semanticsroom 217, not Sloman Lounge Achim Jung (School of Computer Science). 217, School of Computer Science. Friday 02 February 2018, 11:00-12:00 ## Some remarks on n-fibrationsSina Hazratpour, CS Theory Group Birmingham. Tuesday 30 January 2018, 13:00-14:00 ## Teaching old type systems new tricks with type providersTomas Petricek (Alan Turing Institute). Computer Science, The Sloman Lounge (UG). Friday 26 January 2018, 11:00-12:00 ## Linear typings as flows on 3-valent graphs (Part 1: imploids and flows)Note not usual room Noam Zeilberger, CS Theory Group Birmingham. Tuesday 23 January 2018, 13:00-14:00 ## Spaces of alpha-Lipschitz continuous maps, in a quasi-metric setting.Jean Goubault-Larrecq (LSV, ENS Paris-Saclay). Computer Science, The Sloman Lounge (UG). Friday 19 January 2018, 11:00-12:00 ## From curves to train tracks to compressed wordsNB 217 not Sloman Lounge Saul Schleimer (Maths, Warwick). 217, School of Computer Science. Friday 12 January 2018, 11:00-12:00 ## A Curry-Howard Correspondence for Event-Based ProgrammingNeel Krishnaswami (University of Cambridge, formerly Birmingham). Computer Science, The Sloman Lounge (UG). Friday 08 December 2017, 11:00-12:00 ## A syntactic view of adequacyMarco Devesas Campos, CS Theory Group. Wednesday 06 December 2017, 13:00-14:00 ## Universally optimal mitigation strategies for leakage of informationPasquale Malacaria (Queen Mary, London). Computer Science, The Sloman Lounge (UG). Friday 01 December 2017, 11:00-12:00 ## Syntactic and semantic fun with monadsFredrik Dahlqvist (UCL). Computer Science, The Sloman Lounge (UG). Friday 24 November 2017, 11:00-12:00 ## Using Yoneda rather than J to present the identity type.Martin Escardo, CS Theory Group Birmingham. Wednesday 22 November 2017, 01:00-02:00 ## A concurrent interpretation of the law of excluded middleUlrich Berger (University of Swansea). Computer Science, The Sloman Lounge (UG). Friday 17 November 2017, 11:00-12:00 ## Decidable Logics for Path Feasibility of Programs with StringsAnthony Widjaja Lin (University of Oxford). Computer Science, The Sloman Lounge (UG). Friday 10 November 2017, 11:00-12:00 ## A sequent calculus for a semi-associative lawTime changed - sorry Noam Zeilberger, Birmingham Theory Group. Wednesday 08 November 2017, 12:00-01:00 ## Segal-type models of higher categoriesSimona Paoli (University of Leicester). Computer Science, The Sloman Lounge (UG). Friday 03 November 2017, 11:00-12:00 ## Free d-frames and quotientsTomas Jakl, CS Theory Group Birmingham/Charles University Prague. Wednesday 01 November 2017, 13:00-01:00 ## Taming poultry, an attempt to use Coq for teaching mathematicians about (assisted) proofsCorneliu Hoffman (University of Birmingham). Computer Science, The Sloman Lounge (UG). Friday 27 October 2017, 11:00-12:00 ## From finitary monads to Lawvere theories: Cauchy completionsNB 217 not Sloman Lounge John Power (University of Bath). 217, School of Computer Science. Friday 20 October 2017, 11:00-12:00 ## No formal presentation (offers welcome!)Speaker to be confirmed. Wednesday 18 October 2017, 01:00-02:00 ## Theoretical Computer Science in Quantum Circuit DesignAlso of interest in Security Peter Hines (University of York). Computer Science, The Sloman Lounge (UG). Friday 13 October 2017, 11:00-12:00 ## Multiplication is commutative, geometricallyNote non-standard time and room Martin Escardo, Birmingham. Wednesday 11 October 2017, 12:00-13:00 ## Realizability in Cyclic Proof: Extracting Ordering Information for Infinite DescentReuben Rowe (University of Kent at Canterbury). Computer Science, The Sloman Lounge (UG). Friday 06 October 2017, 11:00-12:00 ## What kind of virtual machine would be needed to simulate an ancient mathematician investigating geometry?Aaron Sloman (School of Computer Science, bham). Computer Science, The Sloman Lounge (UG). Friday 29 September 2017, 11:00-12:00 ## Type theory without exponentialsSteve Vickers, CS Theory Group Birmingham. Wednesday 27 September 2017, 12:00-13:00 ## Analysis in univalent type theoryAuke Booij, CS Theory Group, Birmingham. Thursday 14 September 2017, 12:00-13:00 ## Towards abductive functional programmingKoko Muroya, CS Theory Group, University of Birmingham. Thursday 31 August 2017, 12:00-13:00 ## Fibrations of toposesNB This talk is at the theory seminar time (11.0 Friday) in the lab lunch room (217). Sina Hazratpour, CS Theory Group Birmingham. Friday 25 August 2017, 11:00-12:00 ## Locally graded categoriesPaul Levy, CS Theory Group, Birmingham. Thursday 24 August 2017, 12:00-13:00 ## Locally graded categoriesNB This talk is at the theory seminar time (11.0 Friday) in the lab lunch room (217). Paul Levy, CS Theory Group, Birmingham. Friday 18 August 2017, 11:00-12:00 ## Dynamic Geometry of InteractionKoko Muroya, University of Birmingham. Thursday 10 August 2017, 12:00-13:00 ## Partial functions and recursion via dominances in univalent type theoryCory Knapp. Thursday 03 August 2017, 12:00-13:00 ## String diagrams for stably compact localesNB This talk is at the theory seminar time (11.0 Friday) in the lab lunch room (217). Steve Vickers, CS Theory Group Birmingham. Friday 28 July 2017, 11:00-12:00 ## String diagrams for stably compact localesSteve Vickers, CS Theory Group, Birmingham. Thursday 27 July 2017, 12:00-13:00 ## Commutative or monoidal monadsPaul Taylor (U of Brum (honorary)). Thursday 13 July 2017, 12:00-13:00 ## Deciding subtype entailmentStephen Dolan (Computer Lab, University of Cambridge). Computer Science, The Sloman Lounge (UG). Friday 16 June 2017, 11:00-12:00 ## Can we machine-learn a programming language semantics?Dan Ghica (Computer Science). Thursday 08 June 2017, 12:00-13:00 ## New foundations for string diagram rewritingFabio Zanasi (UCL). Computer Science Sloman Lounge. Friday 02 June 2017, 11:00-12:00 ## Relative pseudomonadsRoom change! Nicola Gambino (University of Leeds). Friday 26 May 2017, 11:00-12:00 ## Adjunctions that are both monadic and comonadicPostponed and moved. Paul Taylor (U of Brum (honorary)). Thursday 25 May 2017, 11:59-13:00 ## Algorithms and barriers for random instances of computational problemsWill Perkins (Dept of Mathematics, University of Birmingham). Computer Science Sloman Lounge. Friday 19 May 2017, 11:00-12:00 ## Solution of an old problem in vector optimisation: Support function of the generalised JacobianAbbas Edalat (Imperial College). Computer Science Sloman Lounge. Friday 28 April 2017, 11:00-12:00 ## A Geometry of Interaction semantics for TensorFlowDan Ghica (University of Birmingham). Computer Science Sloman Lounge. Friday 07 April 2017, 11:00-12:00 ## Some enumerative, topological, and algebraic aspects of linear lambda calculusNoam Zeilberger, SoCS UoB. Thursday 06 April 2017, 12:00-13:00 ## The frame generated by closed sublocalesAles Pultr (Charles University, Prague). Computer Science Sloman Lounge. Friday 31 March 2017, 11:00-12:00 ## Coalgebraic Dynamic LogicsClemens Kupke (University of Strathclyde). Computer Science Sloman Lounge. Friday 24 March 2017, 11:00-12:00 ## On the commutativity of the powerspace monadsMatthew de Brecht (University of Kyoto). Computer Science Sloman Lounge. Friday 17 March 2017, 11:00-12:00 ## Towards the verified compilation of LustreTimothy Bourke (Inria Paris, École Normale Supérieure). Computer Science, The Sloman Lounge (UG). Friday 10 March 2017, 11:00-12:00 ## Computability and recursion theory in univalent type theoryRoom as usual, despite earlier announcement Cory Knapp, SoCS, Birmingham. Thursday 02 March 2017, 12:00-13:00 ## Closure of system T under the bar recursion rulePaulo Oliva (Queen Mary, University of London). Computer Science, The Sloman Lounge (UG). Friday 24 February 2017, 11:00-12:00 ## Homotopy coherent distributive lawsNick Gurski (University of Sheffield). Computer Science Sloman Lounge. Friday 17 February 2017, 11:00-12:00 ## Computability and recursion theory in univalent type theoryNote change of date (was scheduled for 2 Feb, then 9 Feb) Cory Knapp. Computer Science, The Sloman Lounge (UG). Friday 10 February 2017, 11:00-12:00 ## Functoriality of modified realizabilityRoom 245 not Sloman Lounge Peter Johnstone (DPMMS, University of Cambridge). Friday 03 February 2017, 11:00-12:00 ## Partial functions via dominances in univalent type theoryNote that Cory's talk has been postponed a week, to 9 Feb. Martin Escardo, School of Computer Science, UoBirmingham. Thursday 02 February 2017, 12:00-13:00 ## Partial functions via dominances in univalent type theoryMartin Escardo, School of Computer Science, UoBirmingham. Thursday 26 January 2017, 12:00-13:00 ## Grothendieck toposes fibred over elementary toposesRoom changed Steve Vickers, School of Computer Science, University of Birmingham. Thursday 19 January 2017, 12:00-13:00 ## Reversible System TIan Mackie (University of Sussex). Computer Science, The Sloman Lounge (UG). Friday 13 January 2017, 11:00-12:00 ## Representations for feasibly approximable functionsMichal Konečný (Aston University). Computer Science, The Sloman Lounge (UG). Friday 16 December 2016, 11:00-12:00 ## Type theoretic aspects of AU sketchesApologies for wrong announcement that it was Wednesday Steve Vickers, SoCS, Birmingham. Thursday 15 December 2016, 12:00-13:00 ## A Categorical Perspective on Type Refinement SystemsNoam Zeilberger (University of Birmingham). Thursday 08 December 2016, 12:00-13:00 ## Interaction morphismsTarmo Uustalu (Institute of Cybernetics, Tallinn University of Technology). Computer Science, The Sloman Lounge (UG). Friday 02 December 2016, 11:00-12:00 ## Probabilistic ProgrammingHongseok Yang (University of Oxford). Computer Science, The Sloman Lounge (UG). Friday 25 November 2016, 11:00-12:00 ## Physical/evolutionary foundations for mathematics vs logico/semantic foundations for mathematicsAaron Sloman (University of Birmingham). Computer Science, The Sloman Lounge (UG). Friday 11 November 2016, 11:00-12:00 ## Parametricity for category theoryUday Reddy (School of Computer Science). Thursday 10 November 2016, 12:00-13:00 ## Semantic Foundations for Probabilistic ProgrammingSam Staton (University of Oxford). Computer Science, The Sloman Lounge (UG). Friday 04 November 2016, 11:00-12:00 ## A domain-theoretic approach to Brownian motion and general continuous stochastic processesPaul Bilokon. Computer Science, The Sloman Lounge (UG). Friday 21 October 2016, 11:00-12:00 ## Type theory for the arithmetic universe sketchesDr Steve Vickers (School of Computer Science, University of Birmingham). Thursday 20 October 2016, 12:00-13:00 ## Formalizing compositional proofsJamie Vicary (University of Oxford). Computer Science, The Sloman Lounge (UG). Friday 14 October 2016, 11:00-12:00 ## Title to be confirmedDr Steve Vickers (School of Computer Science, University of Birmingham). Thursday 13 October 2016, 12:00-13:00 ## Reconciling structural and nominal syntax in the language of diagramsDan Ghica (Computer Science). Computer Science, The Sloman Lounge (UG). Friday 07 October 2016, 11:00-12:00 ## Adjunctions and Actions of Co/Cartesian CategoriesFrancisco Lobo (University of Manchester). Computer Science, The Sloman Lounge (UG). Friday 30 September 2016, 11:00-12:00 ## Trace equivalence of well-founded processes via commutativityPaul Levy (University of Birmingham). Thursday 29 September 2016, 12:00-13:00 ## A revised graph syntax from traced monoidal categoriesAliaume Lopez, École normale supérieure. Friday 15 July 2016, 11:00-12:00 ## Jung-Tix problem in sober dcposXiaodong Jia (School of Computer Science, University of Birmingham). Wednesday 06 July 2016, 13:00-14:00 ## Possible world semantics for heap storagePaul Levy (University of Birmingham). Friday 01 July 2016, 13:00-14:00 ## Possible world semantics for heap storagePaul Levy (University of Birmingham). Wednesday 29 June 2016, 13:00-14:00 ## Dynamic games and strategiesNorihiro Yamada (Oxford). Computer Science, The Sloman Lounge (UG). Friday 20 May 2016, 11:00-12:00 ## Sketches for arithmetic universesDr Steve Vickers (School of Computer Science, University of Birmingham). Wednesday 18 May 2016, 13:00-14:00 ## Fibrations in Category Theory and TopologySina (University of Birmingham, UK). Wednesday 06 April 2016, 13:00-14:00 ## Lightweight Cryptography for Next Generation Vehicle Electrical ArchitectureAndrea Radu. Wednesday 02 March 2016, 13:00-14:00 ## Type Theory in Type Theory using Quotient Inductive TypesAmbrus Kaposi (Nottingham). Computer Science, The Sloman Lounge (UG). Friday 26 February 2016, 11:00-12:00 ## Enriched-adjunction models and polarisation for modelling effects and resourcesGuillaume Munch-Maccagnoni (Cambridge). Computer Science, The Sloman Lounge (UG). Friday 19 February 2016, 11:00-12:00 ## Effects as sessions, sessions as effectsDominic Orchard (Imperial). Computer Science, The Sloman Lounge (UG). Friday 12 February 2016, 11:00-12:00 ## Is Mathematics Parametric?Uday Reddy (School of Computer Science). Wednesday 03 February 2016, 13:00-14:00 ## Programming and Proving with Concurrent ResourcesIlya Sergey (UCL). Computer Science, The Sloman Lounge (UG). Friday 29 January 2016, 11:00-12:00 ## NetKAT: A FORMAL SYSTEM FOR THE VERIFICATION OF NETWORKSAlexandra Silva (UCL). Friday 15 January 2016, 11:00-12:00 ## Liveness for programs with higher-order stateNeel Krishnaswami (). Wednesday 13 January 2016, 13:00-14:00 ## Structural Resolution meets Curry-HowardEkaterina Komendantskaya (Dundee). Friday 06 November 2015, 13:00-14:00 ## Improving proof compression by better controlling cut and sharingPaola Bruscoli (Bath). Friday 16 October 2015, 15:00-16:00 ## Continuity and dcpo-completion of posetsZhongxi Zhang, Hunan University visitor. Tuesday 29 September 2015, 12:00-13:00 ## On the Forwarding Paths Produced by Internet Routing AlgorithmsTimothy Griffin (Cambridge). Friday 25 September 2015, 13:00-14:00 ## An educational proof checkerYu Yang Lin, University of Birmingham. Tuesday 22 September 2015, 12:00-13:00 ## Strong Complementarity in Quantum ComputingRoss Duncan (University of Strathclyde). Friday 18 September 2015, 14:00-15:00 ## Categorical probability theory and categorical entropySina Hazratpur. Tuesday 15 September 2015, 12:00-13:00 ## localised side-effects using binding handlers (contd)Bram Geron (University of Birmingham, School of Computer Science). Friday 11 September 2015, 12:00-13:00 ## The recursion hierarchy for PCF is strictJohn Longley (Edinburgh). Tuesday 08 September 2015, 11:00-13:00 ## Diagrammatic mathematics and signal flow graphsPawel Sobocinski (Southampton). Friday 04 September 2015, 15:00-16:00 ## localised side-effects using binding handlersBram Geron (University of Birmingham, School of Computer Science). Monday 31 August 2015, 12:00-13:00 ## Distribution monads, contexuality, and cohomology: part 2Sina Hazratpur. Friday 21 August 2015, 12:30-13:30 ## Distribution monads, contexuality, and cohomologySina Hazratpur. Friday 14 August 2015, 12:00-13:00 ## FreshMLTT: Dependent Type Theory with Names and Name-AbstractionAndy Pitts (University of Cambridge). Friday 08 May 2015, 16:00-17:00 ## Nominal techniques for variables with interleaving scopesDan Ghica (Computer Science). Tuesday 28 April 2015, 12:00-13:00 ## Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent ReasoningRalf Jung (MPI-SWS). Tuesday 21 April 2015, 12:00-13:00 ## Coeffects: Context-aware programming languagesTomas Petricek (University of Cambridge). Friday 20 March 2015, 16:00-17:00 ## A continuous computational interpretation of type theoriesChuangjie Xu (University of Birmingham). Monday 09 March 2015, 12:00-13:00 ## Did Brouwer really mean the BHK interpretation?Martin Escardo (). Tuesday 03 March 2015, 12:00-13:00 ## Automata over infinite alphabetsNikos Tzevelekos (Queen Mary University). Friday 27 February 2015, 16:00-17:00 ## 4-valued coalgebraic modal logic - project descriptionTomas Jakl. Tuesday 24 February 2015, 12:00-13:00 ## Worldly Type SystemsConor McBride (University of Strathclyde). Friday 06 February 2015, 16:00-17:00 ## On Cubes and TypesThorsten Altenkirch (University of Nottingham). Friday 30 January 2015, 16:00-17:00 ## Cohomology of Contextuality and Logical ParadoxesKohei Kishida, University of Oxford. Friday 23 January 2015, 16:00-17:00 ## Innocent Strategies are Sheaves over PlaysTakeshi Tsukada (University of Oxford). Friday 12 December 2014, 12:00-13:00 ## Call-by-Value in a Basic Logic for InteractionSpeaker to be confirmed. Wednesday 12 November 2014, 15:00-16:00 ## A Synchronous Functional Language with Integer ClocksAdrien Guatto, ENS. Monday 06 October 2014, 11:00-12:00 ## Distributing the SECD machineBertie Wheen, University of Birmingham. Friday 26 September 2014, 11:00-12:00 ## Syntax and Semantics of Linear Dependent TypesMatthijs Vakar (University of Oxford). Friday 25 July 2014, 14:00-15:00 ## Reconstructing Observational Type TheoryNeel Krishnaswami (University of Birmingham). Thursday 10 July 2014, 14:00-15:00 ## Local Compactness and Bases in Various Formulations of TopologyPaul Taylor (). Friday 27 June 2014, 13:00-14:00 ## Synthetic domain theory versus N^\infty-setsProf Mojgan Mahmoudi (Shahid Beheshti University). Thursday 26 June 2014, 14:00-15:00 ## Functional programming with effects: what works, what doesn't, how to improveBram Geron (University of Birmingham, School of Computer Science). Tuesday 13 May 2014, 13:00-14:00 ## Geometric constructions preserving fibrationsDr Steve Vickers (School of Computer Science, University of Birmingham). Monday 28 April 2014, 13:00-14:00 ## Linearity and Dependent TypesNeel Krishnaswami (University of Birmingham). Tuesday 01 April 2014, 13:00-14:00 ## A bridge between semiringsFlavien Breuvart, PPS, University of Paris 7. Friday 21 March 2014, 16:00-17:00 ## Logical Relations and Parametricity: A Reynolds Programme for Category Theory and Programming LanguagesUday Reddy (School of Computer Science). Tuesday 18 March 2014, 13:00-14:00 ## Update monads: cointerpreting directed containersTarmo Uustalu, Tallinn University of Technology. Friday 14 March 2014, 14:00-15:00 ## M-Sets, continuedMojgan Mahmoudi (Department of Mathematics, Shahid Beheshti University, Iran.). Friday 21 February 2014, 13:00-14:00 ## GADTs and the Girard/Schroeder-Heister EqualityNeel Krishnaswami (University of Birmingham). Friday 07 February 2014, 13:00-14:00 ## Transitition Systems Over GamesPaul Levy (University of Birmingham). Friday 17 January 2014, 13:00-14:00 ## An introduction to overt subspaces of R^nPaul Taylor, University of Birmingham. Thursday 16 January 2014, 16:00-17:00 ## General Purpose Programming with Dependent TypesEdwin Brady, University of St Andrews. Friday 10 January 2014, 16:00-17:00 ## Characterizing po-monoids $S$ by completeness and injectivity of $S$-posetsMojgan Mahmoudi (Department of Mathematics, Shahid Beheshti University, Iran.) . Friday 20 December 2013, 13:00-14:00 ## The dual of pattern matching - copattern matchingAnton Setzer, Swansea University. Friday 22 November 2013, 16:00-17:00 ## When is the Kleene--Kreisel hierarchy full?Chuangjie Xu (University of Birmingham). Friday 22 November 2013, 13:00-14:00 ## Weakly dependent bounded linear typesFredrik Nordvall Forsberg. Tuesday 19 November 2013, 13:00-14:00 ## Weakly dependent bounded linear typesFredrik Nordvall Forsberg . Tuesday 12 November 2013, 13:00-14:00 ## Two extensions of Reynolds' Relational Parametricity: Classical Mechanics and Dependent TypesBob Atkey. Friday 08 November 2013, 16:00-17:00 ## A reversible pi calculus for concurrent dynamic slicingRoly Perera (University of Birmingham). Tuesday 05 November 2013, 13:00-14:00 ## Product representation of default bilatticesHilary Priestley, University of Oxford. Friday 01 November 2013, 16:00-17:00 ## Title to be confirmedNeel Krishnaswami (University of Birmingham). Tuesday 29 October 2013, 11:00-12:00 ## Distributed abstract machinesOlle Fredriksson, University of Birmingham. Tuesday 22 October 2013, 11:00-12:00 ## Parametric completeness for separation theories (via hybrid logic)James Brotherston, University College London. Friday 18 October 2013, 16:00-17:00 ## A Tribute to John Reynolds IIUday Reddy (School of Computer Science). Tuesday 30 July 2013, 11:00-12:00 ## Axiomatization using locality and free choiceKamal Lodaya, The Institute of Mathematical Sciences, Chennai. Tuesday 16 July 2013, 11:00-12:00 ## Reflection in sheaf modelsMichael Fourman, University of Edinburgh. Thursday 04 July 2013, 14:00-15:00 ## Graphical Foundations for Dialogue GamesCai Wingfield, University of Bath. Friday 17 May 2013, 16:00-17:00 ## Concurrent Games with SymmetryJoint Theory Seminar / Lab Lunch Pierre Clairambault, University of Cambridge. Tuesday 23 April 2013, 11:00-12:00 ## Fibrational parametricityNeil Ghani, University of Strathclyde. Thursday 18 April 2013, 10:00-11:00 ## The Ramifications of Sharing in Data StructuresJules Villard, UCL. Friday 15 March 2013, 16:00-17:00 ## Abstract machines for game semantics, revisitedOlle Fredriksson (University of Birmingham). Tuesday 05 February 2013, 11:00-12:00 ## Decision problems for linear recurrence sequencesJames Worrell, University of Oxford. Friday 01 February 2013, 16:00-17:00 ## Frank, a direct style language with typed effectsConor McBride, University of Strathclyde. Friday 11 January 2013, 16:00-17:00 ## Compositional algebras of C/E and P/T netsPawel Sobocinski, University of Southampton. Friday 30 November 2012, 16:00-17:00 ## Geometry of Synthesis V : PipelinesDan Ghica (Computer Science). Tuesday 27 November 2012, 12:00-13:00 ## Agent programming languagesNatasha Alechina, University of Nottingham. Friday 16 November 2012, 16:00-17:00 ## Functional Semantics of Parsing Actions, and Left Recursion Elimination as Continuation PassingDr Hayo Thielecke (Computer Science). Monday 17 September 2012, 11:00-12:00 ## Operational semantics for signal handlingMaxim Strygin, University of Birmingham. Tuesday 28 August 2012, 12:00-13:00 ## Concurrent Computational Interpretation of Dummett's Axiom and PrelinearityYoichi Hirai, University of Tokyo. Monday 27 August 2012, 11:00-12:00 ## Fibrations and Logical RelationsUnusual time and place! Claudio Hermida. Tuesday 21 August 2012, 15:00-16:00 ## A Voyage to the Deep-HeapDino Distefano, Queen Mary, University of London. Friday 10 August 2012, 16:00-17:00 ## Forcing, effects and continuityMartin Escardo, University of Birmingham. Friday 03 August 2012, 16:00-17:00 ## The value of the two valuesJoão Marcos, Universidade Federal do Rio Grande do Norte. Wednesday 18 July 2012, 16:00-17:00 ## Self-explaining computationUnusual date/venue Roly Perera (University of Birmingham). Monday 09 July 2012, 12:00-13:00 ## Analysing PCF and Kleene computability via sequential proceduresJohn Longley, University of Edinburgh. Friday 06 July 2012, 16:00-17:00 ## Modes of Bar RecursionTom Powell, Queen Mary, University of London. Tuesday 03 July 2012, 16:00-17:00 ## Geometric constructions for (op)fibrationsBertfried Fauser, University of Birmingham. Friday 22 June 2012, 16:00-17:00 ## Abstract machine semantics of regular expression matchingAsiri Rathnayake. Tuesday 19 June 2012, 12:00-13:00 ## Linear dependent types: Complexity of PCF term evaluation.Joint Theory Seminar and Lab Lunch Barbara Petit, Università di Bologna. Monday 11 June 2012, 14:00-15:00 ## Linear dependent types: Complexity of PCF terms evaluationJoint Lab-Lunch and Theory Seminar Barbara Petit, Bologna. Monday 11 June 2012, 14:00-15:00 ## Multiparty session types and distributed systemsNobuko Yoshida, Imperial College London. Friday 01 June 2012, 16:00-17:00 ## A Saturation Method for Collapsible Pushdown SystemsJoint Theory Seminar and Lab Lunch Matthew Hague, Université Paris-Est. Tuesday 29 May 2012, 12:00-13:00 ## Title to be confirmedJoint Lab Lunch and Theory seminar Matt Hague, Paris. Tuesday 29 May 2012, 12:00-13:00 ## Measuring progress of probabilistic model-checkersFranck van Breugel, York University, Toronto. Thursday 05 April 2012, 16:00-17:00 ## Parameterized algebraic theories and computational effectsSam Staton, University of Cambridge. Friday 09 March 2012, 16:00-17:00 ## Automata and logics on structures with dataRanko Lazic, University of Warwick. Friday 24 February 2012, 16:00-17:00 ## Observations about definability in an abstract datatype of real numbersAlex Simpson, University of Edinburgh. Friday 03 February 2012, 13:00-14:00 ## Call-by-push-value tutorial [part 4]Paul Levy (University of Birmingham). Tuesday 31 January 2012, 12:00-13:00 ## Topological dualities for distributive meet-semilattices, implicative semilattices and Hilbert algebrasRamon Jansana, University of Barcelona. Friday 20 January 2012, 16:00-17:00 ## Constructing Differential Categories and Deconstructing Categories of GamesGuy McCusker, University of Bath. Friday 13 January 2012, 16:00-17:00 ## When is a Container a Comonad?Danel Ahman, University of Cambridge. Tuesday 13 December 2011, 12:00-13:00 ## Suszko's Thesis and ExtensionalityMatteo Bianchetti, University of St Andrews. Friday 09 December 2011, 16:00-17:00 ## The language X: term rewriting, continuations and classical types, and the impossibility of filter semanticsSteffen van Bakel, Imperial College London. Friday 25 November 2011, 16:00-17:00 ## The valuation locale monad (continued)Dr Steve Vickers (School of Computer Science, University of Birmingham). Tuesday 22 November 2011, 12:00-13:00 ## Induction and Coinduction in fibrationsClément Fumex, University of Strathclyde. Friday 18 November 2011, 16:00-17:00 ## How To Be More ProductiveGraham Hutton, University of Nottingham. Friday 11 November 2011, 16:00-17:00 ## Inductive-inductive definitions: axiomatisation and categorical semanticsFredrik Nordvall Forsberg, Swansea University. Friday 28 October 2011, 16:00-17:00 ## Understanding Multi-core ConcurrencyScott Owens, University of Cambridge. Friday 21 October 2011, 16:00-17:00 ## Towards a Categorical Foundation for Generic ProgrammingRalf Hinze, University of Oxford. Tuesday 18 October 2011, 13:00-14:00 ## A monad of valuation locales IIDr Steve Vickers (School of Computer Science, University of Birmingham). Tuesday 11 October 2011, 12:00-13:00 ## A monad of valuation locales I : Introduction and motivationDr Steve Vickers (School of Computer Science, University of Birmingham). Tuesday 04 October 2011, 12:00-13:00 ## Are all substitutions invertible; are all monoids groups?Murdoch Gabbay, Heriot-Watt University. Friday 23 September 2011, 13:00-14:00 ## Towards a localic proof of the localic groupoid representation of Grothendieck toposesChristopher Townsend. Friday 02 September 2011, 16:00-17:00 ## Imperative Programs as Proofs via Game SemanticsMartin Churchill, University of Bath. Friday 08 July 2011, 16:00-17:00 ## Towards a Geometry of Interaction for Polarized Linear LogicPhil Scott, University of Ottawa. Friday 01 July 2011, 16:00-17:00 ## Algebraic Foundations for Type and Effect AnalysisOhad Kammar, University of Edinburgh. Thursday 23 June 2011, 14:00-15:00 ## A Statistical Test for Information Leaks Using Continuous Mutual InformationTom Chotia . Tuesday 14 June 2011, 12:00-13:00 ## From Containers to Induction RecursionNeil Ghani, University of Strathclyde. Friday 03 June 2011, 16:00-17:00 ## A Categorical Compositional Distributional Model of Meaning and some Supporting ExperimentsMehrnoosh Sadrzadeh, University of Oxford. Friday 20 May 2011, 16:00-17:00 ## Verification of Quantum MechanicsElham Kashefi, University of Edinburgh. Friday 06 May 2011, 16:00-17:00 ## Energy as SyntaxJoint Theory/School Seminar Vincent Danos, University of Edinburgh. Thursday 05 May 2011, 16:00-17:00 ## Protocol security, deducibility constraints and algebraic propertiesSergiu Bursuc (Computer Science). Tuesday 29 March 2011, 13:00-14:00 ## Systems and Security Modelling: From Theory to Practice (Really)David Pym, University of Aberdeen. Friday 18 March 2011, 16:00-17:00 ## Automatic program analysis for overlaid data structuresHongseok Yang, Queen Mary, University of London. Friday 11 March 2011, 16:00-17:00 ## Approximating Labelled Markov Processes by AveragingPrakash Panangaden, University of Oxford, on leave from McGill University (Montreal). Friday 04 March 2011, 16:00-17:00 ## Finding vulnerabilities in webapps by string analysisMarco Cova. Tuesday 01 March 2011, 12:00-13:00 ## Ultrametric Semantics of Reactive ProgramsNeel Krishnaswami, Microsoft Research Cambridge. Friday 25 February 2011, 16:00-17:00 ## The Born map for the topos qbit (continued)Bertfried Fauser (Computer Science). Tuesday 22 February 2011, 12:00-13:00 ## Permissive-Nominal LogicMurdoch Gabbay, Heriot-Watt University. Friday 18 February 2011, 16:00-17:00 ## Adventures in XML UpdatesJames Cheney, University of Edinburgh. Friday 04 February 2011, 16:00-17:00 ## Abstraction and Refinement for Local ReasoningThomas Dinsdale-Young, Imperial College London. Friday 28 January 2011, 16:00-17:00 ## Formalizing Domains, Ultrametric Spaces and Semantics of Programming LanguagesNick Benton, Microsoft Research Cambridge. Friday 21 January 2011, 16:00-17:00 ## A topos-theoretic approach to Stone-type dualitiesOlivia Caramello, University of Cambridge. Friday 10 December 2010, 16:00-17:00 ## Information carriers in biomolecular networksVincent Danos, University of Edinburgh. Friday 03 December 2010, 16:00-17:00 ## Semantics of Polymorhism in Imperative ProgrammingUday Reddy. Tuesday 23 November 2010, 12:00-13:00 ## Solving corecursive equationsVenanzio Capretta, University of Nottingham. Friday 19 November 2010, 16:00-17:00 ## Isomorphism of types in presence of higher-order storePierre Clairambault, University of Bath. Friday 12 November 2010, 16:00-17:00 ## Privacy-supporting cloud-based conference systems: protocol and verificationMyrto Arapinis, Sergiu Bursuc and Mark Ryan. Tuesday 09 November 2010, 12:00-13:00 ## Fully Homomorphic EncryptionNigel Smart, University of Bristol. Friday 05 November 2010, 16:00-17:00 ## Concurrent Games on Partial OrdersJulian Gutierrez, University of Edinburgh. Friday 29 October 2010, 16:00-17:00 ## Multicategories, unwirability and gamesNathan Bowler, University of Cambridge. Friday 15 October 2010, 16:00-17:00 ## What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in CommonMartin Escardo. Tuesday 12 October 2010, 12:00-13:00 ## Resource management via type inference in a hardware compilerAlex Smith. Tuesday 05 October 2010, 12:00-13:00 ## Display Calculus for Bunched LogicJames Brotherston, Imperial College London. Friday 24 September 2010, 14:00-15:00 ## Understanding Game Semantics through Coherence SpacesAna Calderon, University of Bath. Friday 27 August 2010, 14:00-15:00 ## Local Action Traces and Abstract Concurrent Separation LogicSteve Brookes, Carnegie Mellon University and Queen Mary, University of London. Friday 23 July 2010, 14:00-15:00 ## Program extraction from proofs using classical dependent choiceMonika Seisenberger, University of Swansea. Thursday 22 July 2010, 10:00-11:00 ## Bilattices: an algebraic (logic) perspectiveUmberto Rivieccio, University of Genoa. Friday 02 July 2010, 14:00-15:00 ## Canonical extensions and Stone duality for strong proximity latticesSam van Gool. Tuesday 29 June 2010, 12:00-13:00 ## When exactly is Scott sober?Weng Kin Ho, National Institute of Education, Singapore. Friday 18 June 2010, 14:00-15:00 ## From observational to symbolic to static equivalenceSergiu Bursuc. Tuesday 08 June 2010, 13:00-14:00 ## A coalgebraic approach to term graphsRichard Garner, University of Cambridge. Friday 04 June 2010, 14:00-15:00 ## Verification of Windows Device DriversSamin Ishtiaq, Microsoft Research Cambridge. Friday 14 May 2010, 14:00-15:00 ## A Fibrational Induction Rule for Inductive TypesPatricia Johann, University of Strathclyde. Tuesday 04 May 2010, 13:00-14:00 ## Metric Spaces, Abstract Interpretation and Termination AnalysisAziem Chawdhary, University of Durham. Friday 30 April 2010, 16:00-17:00 ## The history, nature, and significance of virtual machineryAaron Sloman. Tuesday 23 March 2010, 13:00-14:00 ## Universal algebra over nominal setsDaniela Petrisan, University of Leicester. Friday 12 March 2010, 14:00-15:00 If you have a question about this list, please contact: Benedikt Ahrens; Miriam Backens; Martin Escardo; Achim Jung; Paul Levy; David Parker; Uday Reddy; Eike Ritter; Anupam Das; Dan Ghica; Rajesh Chitnis; Vincent Rahli; Dr Steve Vickers; mxn732; Tom de Jong; Gianluca Curzi; George Kaye. If you have a question about a specific talk, click on that talk to find its organiser. |
## Other listsParticle Physics Seminars Computer Science Distinguished Seminar Metamaterials Research Group Seminars## Other talksCollective phenomena in excitonic quantum matter Optical fiber sensing based on nanostructured coatings Gravitational waves from black holes and neutron stars FnS - Creating noise to remove noise |