|![[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) |
Theoretical computer science seminar
Add to your list(s)
Send you e-mail reminders
Further detail
Seminar series in theoretical computer science 10 upcoming talks and 280 talks in the archive. Some applications of free extensions to partial evaluation, equational-proof synthesis, and normalisation-by-evaluationNote unusual time because of interviews
Effectfully gardening with the PythiaNote unusual time because of interviews
Fundamental Theorem of Calculus, point-free -- applications to exp and log
Composable Constraint Models for Permutation Problems
Control flow as a contour of data flowThis term, seminars will start at 14:00
Cyclic Systems for Arithmetic Theories of Inductive Definitions
When measurable spaces don't have enough points
The linear operator semantics of probabilistic programs
Temporal Refinements for Guarded Recursive Types
The Functional Machine Calculus
Acyclic types and epimorphisms in homotopy type theoryTom day Jong!
Concept-Instance Algebra -- A retelling of B-systems
Mixed states and module categories
Primrose: Selecting Container Data Types by their Properties
The Fine-Grained Complexity of Pattern Counting Problems
Kripke Semantics for Intuitionistic Łukasiewicz Logic
Model Theory ex Proof-search
Model Counting meets F0 Estimation
Zigzag games, alternating infinite word automata and linear Monadic-Second order logic
Implicit automata in typed λ-calculi
Transducers of polynomial growth
Recent results and open questions in applied proof theory
The Berry Order (ideas from 1980s stable domain theory)
Cyclic Proofs, Hypersequents, and Transitive Closure Logic
Seemingly impossible programs and proofs
Comprehension bicategories
Constructing fully-abstract models of effectful λ-calculi
Synthetic fibered (∞,1)-category theory
Confluence with basic effects
From axioms to synthetic inference rules via focusing
Categorifying Intersection Types
A Type Theory for Strictly Associative Infinity Categories
Solving Verification Questions using Machine Learning
Types are Internal oo-Groupoidshttps://bham-ac-uk.zoom.us/j/83662748860?pwd=dTBRV1JCUEgxQXV1cXpjV3pDaGttUT09
The Strange Career of Interpolation and Definability
Logic beyond formulas: a proof system on graphs
Canonical proof-objects for coinductive programming
Hierarchical string diagram for closed monoidal categories
Hierarchical string diagrams for closed monoidal categories
Automatic differentiation in string diagrams
Proof complexity of positive branching programs
Adelic Geometry via Topos Theory (note change in time!)
New minimal linear inferences in Boolean logic independent of switch and medial
The smash product of monoidal theories
Environments & CPS translations, a well-typed story
On the proof theory of conditional logics
Reparametrizing gradient descent
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.
A minimal cyclic formal framework for coinduction
Arithmetic universes: Home of free algebrasGiven as invited contribution to the Erik Palmgren memorial conference, 19-21 Nov 2020
Extracting nested relational queries from implicit definitions
On program equivalence in the probabilistic lambda calculus
Lovász' Theorem and Comonads in Finite Model TheoryThe talk is at 2pm. We start at 1:50 for socializing with the speaker.
Intutions on domain theory and geometry
Quantitative Tauberian theorems
An Authoritarian Approach to Presheaves
Elementary doctrines as coalgebras
Synthetic probability theory
Formalising mathematics in a theorem prover
Near-Optimal Complexity Bounds for Fragments of the Skolem Problem
Identity, indiscernibility, and univalence: a higher structure identity principle
Trace Theory for Probability and Nondeterminism
ZX-calculus and its applications
From Brouwer's Thesis to the Fan Functional
Consistency of circuit lower bounds with bounded theories
Gödel's incompleteness theorem using arithmetic universeschange of venue
Induction for Cycles
On the complexity of linear arithmetic theories over the integers
Constructing Infinitary Quotient-Inductive Types
Taylor expansion in linear logic is invertible: A completeness result
Nested proof systems for modal logics (and beyond)
Algorithmic Human Development: What is it and why do we need it now?Note unusual time
On the logical complexity of cyclic arithmetic
Diagram rewriting in double categories
Foundational end-to-end verification of cyber-physical systems: The VeriPhy pipeline and its Applications
Constructive Brouwer Fixed Point Theorem
Rudimentary recursion
A Sound and Complete Logic for Algebraic Effects
Geometric morphisms as structure preserving maps and other nice characterisations
Reasoning about effectful programs and evaluation order
Reasoning about entailment in natural language data using vectors, density matrices, and category theory
Two Sides of the Same Coin: Session Types and Game Semantics
Graph Theory and the Transfinite
Designing an algebraic effect system for OCaml
Operational approaches to the foundations of physics
Linear Implicative Algebras, a Brouwer-Heyting-Kolmogorov interpretation of linear logic
Proof-Carrying Plans
Unrestricted Quantification and the Structure of Type Theory
COMPUTER PROBLEMS POSED BY DESSINS D'ENFANTS THEORY
Numerically Definite Logic
Strategic Graph Rewriting in PORGY — an interactive modelling framework
Higher Universal Algebra in Type Theory
Towards Coherence for Guarded Traces
Don't Try This at Home: No-Go Theorems for Distributive Laws
Reflection principles in subsystems of analysis
Reverse mathematics of non-deterministic inductive definitions
Polynomials via fibrations
Some Open Problems in Homotopy Type Theory
Quantitative Algebraic Reasoning
Quasitopoi and universes of propositions
Towards a Formal Theory of Renaming for OCaml
Completing the ZX-calculus
Hypergraph categories as cospan algebras
Understanding Girard’s Paradox
A homotopy type theory for directed homotopy theory
Magnitude of Metric Spaces
Future directions for Java
A Unified Perspective of Linear Time Logics using Coalgebras
Ordinals vs. Cardinals in N? and BeyondSpecial seminar arranged by Aaron Sloman
Physical oracles: Measurement, complexity and cyber-physical systems
An Algebraic Combinatorial Approach to the Abstract Syntax of Opetopic Structures
Handlers in Scope with Adjunctions
Concurrent Kleene Algebra: free model and completeness
The Dialectica models of type theoryroom 217, not Sloman Lounge
The Church-Turing Thesis and denotational semanticsroom 217, not Sloman Lounge
Teaching old type systems new tricks with type providers
Spaces of alpha-Lipschitz continuous maps, in a quasi-metric setting.
From curves to train tracks to compressed wordsNB 217 not Sloman Lounge
A Curry-Howard Correspondence for Event-Based Programming
Universally optimal mitigation strategies for leakage of information
Syntactic and semantic fun with monads
A concurrent interpretation of the law of excluded middle
Decidable Logics for Path Feasibility of Programs with Strings
Segal-type models of higher categories
Taming poultry, an attempt to use Coq for teaching mathematicians about (assisted) proofs
From finitary monads to Lawvere theories: Cauchy completionsNB 217 not Sloman Lounge
Theoretical Computer Science in Quantum Circuit DesignAlso of interest in Security
Realizability in Cyclic Proof: Extracting Ordering Information for Infinite Descent
What kind of virtual machine would be needed to simulate an ancient mathematician investigating geometry?
Deciding subtype entailment
New foundations for string diagram rewriting
Relative pseudomonadsRoom change!
Algorithms and barriers for random instances of computational problems
Solution of an old problem in vector optimisation: Support function of the generalised Jacobian
A Geometry of Interaction semantics for TensorFlow
The frame generated by closed sublocales
Coalgebraic Dynamic Logics
On the commutativity of the powerspace monads
Towards the verified compilation of Lustre
Closure of system T under the bar recursion rule
Homotopy coherent distributive laws
Functoriality of modified realizabilityRoom 245 not Sloman Lounge
Reversible System T
Representations for feasibly approximable functions
Interaction morphisms
Probabilistic Programming
Physical/evolutionary foundations for mathematics vs logico/semantic foundations for mathematics
Semantic Foundations for Probabilistic Programming
A domain-theoretic approach to Brownian motion and general continuous stochastic processes
Formalizing compositional proofs
Reconciling structural and nominal syntax in the language of diagrams
Adjunctions and Actions of Co/Cartesian Categories
Dynamic games and strategies
Type Theory in Type Theory using Quotient Inductive Types
Enriched-adjunction models and polarisation for modelling effects and resources
Effects as sessions, sessions as effects
Programming and Proving with Concurrent Resources
NetKAT: A FORMAL SYSTEM FOR THE VERIFICATION OF NETWORKS
Structural Resolution meets Curry-Howard
Improving proof compression by better controlling cut and sharing
On the Forwarding Paths Produced by Internet Routing Algorithms
Strong Complementarity in Quantum Computing
The recursion hierarchy for PCF is strict
Diagrammatic mathematics and signal flow graphs
FreshMLTT: Dependent Type Theory with Names and Name-Abstraction
Coeffects: Context-aware programming languages
Automata over infinite alphabets
Worldly Type Systems
On Cubes and Types
Cohomology of Contextuality and Logical Paradoxes
Innocent Strategies are Sheaves over Plays
A bridge between semirings
Update monads: cointerpreting directed containers
An introduction to overt subspaces of R^n
General Purpose Programming with Dependent Types
The dual of pattern matching - copattern matching
Two extensions of Reynolds' Relational Parametricity: Classical Mechanics and Dependent Types
Product representation of default bilattices
Parametric completeness for separation theories (via hybrid logic)
Reflection in sheaf models
Graphical Foundations for Dialogue Games
Concurrent Games with SymmetryJoint Theory Seminar / Lab Lunch
Fibrational parametricity
The Ramifications of Sharing in Data Structures
Decision problems for linear recurrence sequences
Frank, a direct style language with typed effects
Compositional algebras of C/E and P/T nets
Agent programming languages
Concurrent Computational Interpretation of Dummett's Axiom and Prelinearity
A Voyage to the Deep-Heap
Forcing, effects and continuity
The value of the two values
Analysing PCF and Kleene computability via sequential procedures
Modes of Bar Recursion
Geometric constructions for (op)fibrations
Linear dependent types: Complexity of PCF term evaluation.Joint Theory Seminar and Lab Lunch
Multiparty session types and distributed systems
A Saturation Method for Collapsible Pushdown SystemsJoint Theory Seminar and Lab Lunch
Measuring progress of probabilistic model-checkers
Parameterized algebraic theories and computational effects
Automata and logics on structures with data
Observations about definability in an abstract datatype of real numbers
Topological dualities for distributive meet-semilattices, implicative semilattices and Hilbert algebras
Constructing Differential Categories and Deconstructing Categories of Games
Suszko's Thesis and Extensionality
The language X: term rewriting, continuations and classical types, and the impossibility of filter semantics
Induction and Coinduction in fibrations
How To Be More Productive
Inductive-inductive definitions: axiomatisation and categorical semantics
Understanding Multi-core Concurrency
Towards a Categorical Foundation for Generic Programming
Are all substitutions invertible; are all monoids groups?
Towards a localic proof of the localic groupoid representation of Grothendieck toposes
Imperative Programs as Proofs via Game Semantics
Towards a Geometry of Interaction for Polarized Linear Logic
Algebraic Foundations for Type and Effect Analysis
From Containers to Induction Recursion
A Categorical Compositional Distributional Model of Meaning and some Supporting Experiments
Verification of Quantum Mechanics
Energy as SyntaxJoint Theory/School Seminar
Systems and Security Modelling: From Theory to Practice (Really)
Automatic program analysis for overlaid data structures
Approximating Labelled Markov Processes by Averaging
Ultrametric Semantics of Reactive Programs
Permissive-Nominal Logic
Adventures in XML Updates
Abstraction and Refinement for Local Reasoning
Formalizing Domains, Ultrametric Spaces and Semantics of Programming Languages
A topos-theoretic approach to Stone-type dualities
Information carriers in biomolecular networks
Solving corecursive equations
Isomorphism of types in presence of higher-order store
Fully Homomorphic Encryption
Concurrent Games on Partial Orders
Multicategories, unwirability and games
Display Calculus for Bunched Logic
Understanding Game Semantics through Coherence Spaces
Local Action Traces and Abstract Concurrent Separation Logic
Program extraction from proofs using classical dependent choice
Bilattices: an algebraic (logic) perspective
When exactly is Scott sober?
A coalgebraic approach to term graphs
Verification of Windows Device Drivers
A Fibrational Induction Rule for Inductive Types
Metric Spaces, Abstract Interpretation and Termination Analysis
Universal algebra over nominal sets
Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors
The Continuous π-Calculus: A Process Algebra for Biochemical Modelling
Reconstructing the SECD machine
A Demonic Approach to Information in Probabilistic Systems
A topos-theoretic approach to non-commutative topology
A Unifying Analytical Framework for Discrete Linear TimeJoint Theory/Departmental Seminar
Complex numbers and categorical structures
Linearly-used Continuations and Self-duality
Realisability for Coinduction with Applications in Computable Analysis
First-Order Reasoning about Higher-Order Concurrency
A process algebra for the modelling of hybrid systems
Branching vs Linear Time: Semantical Perspective
Path-Based Coalgebraic Temporal Logics
Providing a Fiction of Disjoint Concurrency
Distributive Laws in Programming Structures
Relative monads
Focusing on Binding and Computation
If you have a question about this list, please contact: George Kaye; Chris Barrett. If you have a question about a specific talk, click on that talk to find its organiser. |
Other listsTheoretical Physics Journal Club Speech Recognition by Synthesis Seminars Topology and Dynamics seminarOther talksGeometry of alternating projections in metric spaces with bounded curvature Modelling uncertainty in image analysis. Quantum simulations using ultra cold ytterbium Ultrafast, all-optical, and highly efficient imaging of molecular chirality Sylow branching coefficients for symmetric groups TBC |
Ohad Kammar (University of Edinburgh).
Friday 24 March 2023, 11:00-11:50