|![[Search]](/images/search.gif?1209136071)
|![[A-Z Index]](/images/az.gif?1209136071)
|![[Contact]](/images/contact.gif?1209136071)
||![[University of Birmingham]](/images/identifier2.gif?1243330508){kind=small} |
![[Talks@bham]](/images/talkslogosmall.gif?1243330508) |
Lab Lunch
Add to your list(s)
Send you e-mail reminders
Further detail
Informal talks for the Theory group in School of Computer Science 0 upcoming talks and 276 talks in the archive. From intuitionistic justification logic to explicit modal type theory with diamond
Learning algorithms versus automatability of Frege systems
Apartness in constructive domain theory: part II
Apartness in constructive domain theory
Regular string-to-string function in the linear λ-calculus
The coherence space semantics of purely linear system F is finite and effective
Semantic evaluation in the simply typed λ-calculus: implicit complexity and normalization
Specker sequences and their relevance to Proof Mining
Teaching complexity theory without machines, some reflections: part II
Teaching complexity theory without machines, some reflections
Part III: Some musings on circular proofs and the metamathematical approach to proof mining and higher-order computability
Part II: Some musings on circular proofs and the metamathematical approach to proof mining and higher-order computability
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.
Circularly typed programs and their abstraction complexity
Combining cyclic proofs and implicit complexity
The Graphical Language of Symmetric Traced Monoidal Categories
Broad Infinity and Generation PrinciplesVirtual Lab Lunch - Passcode: 217
Whisker-based biased composition in infinity categoriesAlex is leaving the School sadly, so this will be his last talk as an internal speaker!
Pointfree Construction of Positive Real Exponentiation
Formal topology and GRD-systems
Formal topology and GRD-systems
Formal Topology in Univalent FoundationsAyberk is a new Ph.D. student with Martín Escardó.
Formalising the Escardó-Simpson Interval Object in UTTPreceded by a coffee break at 13:30
Bifibrations of Polycategories and Classical Linear LogicNOTE the earlier time of 13:30
A Theory of Particular SetsPreceded by a coffee break at 13:30
The ring of adeles from a homotopical viewpointPreceded by a coffee break at 13:30
Booij’s locators point-freehttps://us02web.zoom.us/j/82603907326?pwd=dXlBdmh0RnRZTDc0Zk1pQXhndWI4Zz09
On linear rewriting systems for Boolean logic and some applications to proof theory (2)https://us04web.zoom.us/j/7744570352
Introduction to the ZX-calculus (2)https://us04web.zoom.us/j/7744570352
Introduction to the ZX-calculushttps://us04web.zoom.us/j/498274768 https://us04web.zoom.us/j/305829441
On linear rewriting systems for Boolean logic and some applications to proof theory
Analysis in Univalent Type TheoryThis will be a Virtual Lab Lunch: https://zoom.us/j/615775681
Coinductive Invertibility in Higher Categorieshttps://meet.google.com/ecc-quzw-qyq
Gödel's incompleteness theorem using arithmetic universeschange of venue
The Cantor-Schröder-Bernstein Theorem for ∞-groupoids
Revisiting the relation between subspaces and sublocales
Well founded coalgebras and recursion
Proof complexity through the lens of the pigeon hole principle II
String diagrams for cartesian bicategories and their Karoubi envelopes - and entailment systems
Algorithms and Complexity through the eyes of Vertex Cover (Part 2)Part 2 of last week's talk
Algorithms and Complexity through the eyes of Vertex Cover
Internal higher-categorical models of dependent type theoryPlease contact Todd if you wish to give a talk this term!
A Brouwerian Intuitionistic Type Theory (Part 3)Please contact Todd if you wish to give a talk this term!
A Brouwerian Intuitionistic Type Theory (Part 2)First talk of the term. Please contact Todd if you wish to give a talk this term!
Transparent synchronous dataflow
A Brouwerian Intuitionistic Type Theory
The coproduct of frames as encoding d-frame structure
Denotational Semantics of Linear Logic with Least and Greatest Fixpoints
The lifting monad in infinity-groupoids, or types in univalent mathematicsNote room 245 this week
The lifting monad in infinity-groupoids, or types in univalent mathematicsNote changed time and place, theory seminar slot for lab lunch talk
The Scott model of PCF in UniMathMartin Escardo's talk has been postponed to Friday 22, Sloman Lounge at 11.00
BAGSPACES, (OP)FIBRATIONS, AND COLIMITS OF POINT-FREE GENERALIZED SPACES
BAGSPACES, (OP)FIBRATIONS, AND COLIMITS OF POINT-FREE GENERALIZED SPACES
Bagspaces, (op)fibrations, and colimits of point-free generalized spacesNote room 245
Higher Universal Algebra in Type Theory
Fibrations and opfibrations of generalized point-free spaces
Fibrations and opfibrations of toposes
A foundation for machine learning from Peirce's Logic of Science
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.)
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.
Discrete spaces are opfibrant, Stone spaces are fibrant (categorically) - and why it mattersPostponed from 25 Oct
Compact ordinals in constructive univalent mathematics(Steve Vickers's advertised talk is postponed to next week)
Compact ordinals in constructive univalent mathematicsWe found a room after all!
Formulating categorical concepts using classesContinuation of last week's talk.
Formulating categorical concepts using classes
Postponed (Topological structure in single molecular imaging)POSTPONED - new date not fixed yet.
REBA: A Refinement-Based Architecture for Knowledge Representation and Reasoning in RoboticsNote change of time and room.
(Op)fibrations of toposesRoom changed
Univalent mathematics - continued
Geometric/AU mathematics
Univalent mathematicsNote not usual room
Linear typings as flows on 3-valent graphs (part 3)
Linear typings as flows on 3-valent graphs
Some remarks on n-fibrations
Linear typings as flows on 3-valent graphs (Part 1: imploids and flows)Note not usual room
A syntactic view of adequacy
Using Yoneda rather than J to present the identity type.
A sequent calculus for a semi-associative lawTime changed - sorry
Free d-frames and quotients
No formal presentation (offers welcome!)
Multiplication is commutative, geometricallyNote non-standard time and room
Type theory without exponentials
Analysis in univalent type theory
Towards abductive functional programming
Fibrations of toposesNB This talk is at the theory seminar time (11.0 Friday) in the lab lunch room (217).
Locally graded categories
Locally graded categoriesNB This talk is at the theory seminar time (11.0 Friday) in the lab lunch room (217).
Dynamic Geometry of Interaction
Partial functions and recursion via dominances in univalent type theory
String diagrams for stably compact localesNB This talk is at the theory seminar time (11.0 Friday) in the lab lunch room (217).
String diagrams for stably compact locales
Commutative or monoidal monads
Can we machine-learn a programming language semantics?
Adjunctions that are both monadic and comonadicPostponed and moved.
Some enumerative, topological, and algebraic aspects of linear lambda calculus
Computability and recursion theory in univalent type theoryRoom as usual, despite earlier announcement
Computability and recursion theory in univalent type theoryNote change of date (was scheduled for 2 Feb, then 9 Feb)
Partial functions via dominances in univalent type theoryNote that Cory's talk has been postponed a week, to 9 Feb.
Partial functions via dominances in univalent type theory
Grothendieck toposes fibred over elementary toposesRoom changed
Type theoretic aspects of AU sketchesApologies for wrong announcement that it was Wednesday
A Categorical Perspective on Type Refinement Systems
Parametricity for category theory
Type theory for the arithmetic universe sketches
Title to be confirmed
Trace equivalence of well-founded processes via commutativity
A revised graph syntax from traced monoidal categories
Jung-Tix problem in sober dcpos
Possible world semantics for heap storage
Possible world semantics for heap storage
Sketches for arithmetic universes
Fibrations in Category Theory and Topology
Lightweight Cryptography for Next Generation Vehicle Electrical Architecture
Is Mathematics Parametric?
Liveness for programs with higher-order state
Continuity and dcpo-completion of posets
An educational proof checker
Categorical probability theory and categorical entropy
localised side-effects using binding handlers (contd)
localised side-effects using binding handlers
Distribution monads, contexuality, and cohomology: part 2
Distribution monads, contexuality, and cohomology
Nominal techniques for variables with interleaving scopes
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
A continuous computational interpretation of type theories
Did Brouwer really mean the BHK interpretation?
4-valued coalgebraic modal logic - project description
Call-by-Value in a Basic Logic for Interaction
A Synchronous Functional Language with Integer Clocks
Distributing the SECD machine
Syntax and Semantics of Linear Dependent Types
Reconstructing Observational Type Theory
Local Compactness and Bases in Various Formulations of Topology
Synthetic domain theory versus N^\infty-sets
Functional programming with effects: what works, what doesn't, how to improve
Geometric constructions preserving fibrations
Linearity and Dependent Types
Logical Relations and Parametricity: A Reynolds Programme for Category Theory and Programming Languages
M-Sets, continued
GADTs and the Girard/Schroeder-Heister Equality
Transitition Systems Over Games
Characterizing po-monoids $S$ by completeness and injectivity of $S$-posets
When is the Kleene--Kreisel hierarchy full?
Weakly dependent bounded linear types
Weakly dependent bounded linear types
A reversible pi calculus for concurrent dynamic slicing
Title to be confirmed
Distributed abstract machines
A Tribute to John Reynolds II
Axiomatization using locality and free choice
Abstract machines for game semantics, revisited
Geometry of Synthesis V : Pipelines
Functional Semantics of Parsing Actions, and Left Recursion Elimination as Continuation Passing
Operational semantics for signal handling
Fibrations and Logical RelationsUnusual time and place!
Self-explaining computationUnusual date/venue
Abstract machine semantics of regular expression matching
Linear dependent types: Complexity of PCF terms evaluationJoint Lab-Lunch and Theory Seminar
Title to be confirmedJoint Lab Lunch and Theory seminar
Call-by-push-value tutorial [part 4]
When is a Container a Comonad?
The valuation locale monad (continued)
A monad of valuation locales II
A monad of valuation locales I : Introduction and motivation
A Statistical Test for Information Leaks Using Continuous Mutual Information
Protocol security, deducibility constraints and algebraic properties
Finding vulnerabilities in webapps by string analysis
The Born map for the topos qbit (continued)
Semantics of Polymorhism in Imperative Programming
Privacy-supporting cloud-based conference systems: protocol and verification
What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common
Resource management via type inference in a hardware compiler
Canonical extensions and Stone duality for strong proximity lattices
From observational to symbolic to static equivalence
The history, nature, and significance of virtual machinery
Proving the correctness of a concurrent garbage collector
Symmetries of black box algorithms and combinatorial problem classes
Searchable sets, Dubuc-Penon compactness, the omniscience principle, and the drinker paradox
Title to be confirmed
Clipping: A semantics-directed syntactic approximation
Characterising static equivalence in the applied pi-calculus
Selection functions, bar recursion and backward induction
Localic completion of generalized metric spaces II: Powerlocales
If you have a question about this list, please contact: Dan Ghica; Uday Reddy; Dr Steve Vickers; Paul Taylor; Yuning Feng; Todd Waugh Ambridge; Anupam Das. If you have a question about a specific talk, click on that talk to find its organiser. |
Other listsMathematics Colloquium Chemical Engineering Research Seminar Series Molecular and Medical Physics Seminar SeriesOther talksFrom intuitionistic justification logic to explicit modal type theory with diamond Gravitational waves from black holes and neutron stars FnS - Teaching robots to grasp stuff Collective phenomena in excitonic quantum matter FnS - Creating noise to remove noise Optical fiber sensing based on nanostructured coatings |
Sonia Marin (University of Birmingham).
Thursday 26 May 2022, 14:00-15:00