University of Cambridge > Talks.cam > sb2743's list

sb2743's list

Add to your list(s) Send you e-mail reminders Further detail
Subscribe using ical/vcal (Help)

A personal list of talks.

Tell a friend about this list:

If you have a question about this list, please contact: Siddharth Bhat. If you have a question about a specific talk, click on that talk to find its organiser.

6 upcoming talks and 280 talks in the archive.

Formalisation of mathematics with interactive theorem provers

Can a computer judge interestingness?

(NOTE UNUSUAL DAY/TIME)

UserMichael Douglas (Center of Mathematical Sciences and Applications, Harvard University).

HouseMR15 Centre for Mathematical Sciences.

ClockMonday 29 April 2024, 14:00-15:00

DPMMS Departmental Colloquia

When is a mathematical object well behaved?

UserJulia Wolf (Cambridge).

HouseCMS MR2.

ClockThursday 25 April 2024, 16:00-17:00

Fully in-Place Functional Programming

UserAnton Lorenzen, University of Edinburgh.

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 02 April 2024, 11:00-12:00

Formalisation of mathematics with interactive theorem provers

The Mandelbrot set is connected (and other Lean explorations)

UserDr Geoffrey Irving (previously Google DeepMind, soon the UK AI Safety Institute).

HouseMR14 Centre for Mathematical Sciences.

ClockThursday 29 February 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Experiences with Isabelle/HOL: Formalising Real Algebraic Geometry

UserArtie Khovanov (University of Cambridge), Michael Nedzelsky (Diffblue Ltd) and Dr Wenda Li (University of Edinburgh).

HouseMR14 Centre for Mathematical Sciences.

ClockThursday 22 February 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Structures in dependent type theory

Online

UserProfessor Jeremy Avigad (Carnegie Mellon University).

HouseLive-streamed at MR14 Centre for Mathematical Sciences.

ClockThursday 15 February 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

How to prove Fermat's Last Theorem

Online

UserProfessor Kevin Buzzard (Imperial College London).

HouseLive-streamed at MR14 Centre for Mathematical Sciences.

ClockThursday 08 February 2024, 17:00-18:00

DPMMS Departmental Colloquia

Equidistribution and reciprocity in number theory

UserJack Thorne (Cambridge) .

HouseCMS MR2.

ClockThursday 18 January 2024, 16:00-17:00

Formalisation of mathematics with interactive theorem provers

Towards Autoformalization and Mathematical Reasoning using language models

Note unusual time

UserProfessor Siddhartha Gadgil (Indian Institute of Science).

HouseMR14 Centre for Mathematical Sciences.

ClockWednesday 17 January 2024, 13:00-14:00

Quantum Fields and Strings Seminars

How Non-local is Quantum Gravity? (CANCELLED)

UserAlexandre Belin (U. Milano-Bicocca).

HouseCMS MR2.

ClockThursday 07 December 2023, 10:30-11:30

DPMMS Departmental Colloquia

About random objects in the continuum

UserWendelin Werner (Cambridge).

HouseCMS MR2.

ClockThursday 05 October 2023, 16:00-17:00

Formalisation of mathematics with interactive theorem provers

Roth numbers: Upper, lower bounds, and related constructions

Note: different room, MR20 this time

UserYaël Dillies (University of Cambridge).

HouseMR20 Centre for Mathematical Sciences.

ClockThursday 22 June 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formalizing the change of variables formula for integrals in mathlib

Hybrid talk (please see abstract for link) Note: different room, MR20 this time

UserProfessor Sébastien Gouëzel (Université de Rennes).

HouseMR20 Centre for Mathematical Sciences.

ClockThursday 15 June 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formalizing algebraic number theory, recent progress and future challenges

Note: different room, MR20 this time

UserDr Alex J. Best (King's College London).

HouseMR20 Centre for Mathematical Sciences.

ClockThursday 08 June 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

The leanest automata

Hybrid talk (please see abstract for link) Note: different room, MR20 this time

UserProfessor Bjørn Kjos-Hanssen (University of Hawaii at Manoa).

HouseMR20 Centre for Mathematical Sciences.

ClockThursday 01 June 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Explaining mathematics using formalized mathematics

Hybrid talk (please see abstract for link)

UserProfessor Patrick Massot (Université Paris-Saclay).

House Centre for Mathematical Sciences MR12, CMS.

ClockThursday 18 May 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formalization of diagram chasing as a first-order logic in Coq

Hybrid talk (please see abstract for link)

UserDr Matthieu Piquerez (INRIA, Université de Nantes).

House Centre for Mathematical Sciences MR12, CMS.

ClockThursday 11 May 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Smooth vector bundles in Lean

Hybrid talk (please see abstract for link)

UserProfessor Heather Macbeth (Fordham University).

House Centre for Mathematical Sciences MR12, CMS.

ClockThursday 04 May 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

[CANCELLED] Real Closed Field and Thom Encoding in Isabelle/HOL

[CANCELLED, please check back for rescheduling]

UserDr Wenda Li (University of Cambridge), Artem Khovanov (University of Cambridge) and Michael Nedzelsky (Diffblue Ltd).

House Centre for Mathematical Sciences MR12, CMS.

ClockThursday 09 March 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formalising Turán's Graph Theorem in Isabelle/HOL

Hybrid talk (please see abstract for link)

UserNils Lauermann (INRIA).

House Centre for Mathematical Sciences MR12, CMS.

ClockThursday 02 March 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Some practical problems in formalising mathematics and how to solve them

Hybrid talk (please see abstract for link)

UserDr Manuel Eberl (University of Innsbruck).

House Centre for Mathematical Sciences MR12, CMS.

ClockThursday 09 February 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

The Liquid Tensor Experiment

UserProfessor Kevin Buzzard (Imperial College London).

House Centre for Mathematical Sciences MR12, CMS.

ClockThursday 02 February 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

How Hilbert met Isabelle: Proof Between Generations

Hybrid talk (please see abstract for link)

UserMarco David (École Normale Supérieure de Paris).

House Centre for Mathematical Sciences MR12, CMS.

ClockThursday 26 January 2023, 17:00-18:00

DPMMS Conferences

Categorical Symplectic Topology Conference

UserVarious .

HouseCMS MR2.

ClockMonday 25 March 2019, 09:00-16:30

DPMMS Conferences

Number Theory and Dynamics Conference 2019

UserVarious.

HouseCMS MR2.

ClockMonday 25 March 2019, 09:00-16:30

DPMMS Conferences

British Algebraic Geometry meeting (BrAG)

UserVarious speakers.

HouseCMS MR2.

ClockWednesday 13 September 2017, 09:00-13:15

DPMMS Conferences

British Algebraic Geometry meeting (BrAG)

UserVarious speakers.

HouseCMS MR2.

ClockTuesday 12 September 2017, 09:30-16:00

DPMMS Conferences

British Algebraic Geometry meeting (BrAG)

UserVarious speakers.

HouseCMS MR2.

ClockMonday 11 September 2017, 14:30-21:30

DPMMS Conferences

Tutte Centenary Conference

UserVarious speakers.

HouseCMS MR2.

ClockMonday 10 July 2017, 14:00-21:30

DAMTP Departmental Seminar

Theoretical Implications of the Higgs Discovery

UserGian Giudice, Theoretical Physics Division, CERN.

HouseCMS MR2.

ClockMonday 20 October 2014, 16:30-17:30

Computer Laboratory Automated Reasoning Group Lunches

Logic programming beyond Prolog

This is a MSR Seminar (Station Road), duplicated on the ARG list

UserMaarten van Emden ( University of Victoria, Canada).

HouseSeminar Room, Microsoft Research, Station Road, Cambridge.

ClockThursday 09 October 2014, 14:00-15:00

Semantics Lunch (Computer Laboratory)

Yet more animals: dynamic linkers and debuggers

UserStephen Kell (University of Cambridge).

HouseFW26.

ClockMonday 03 February 2014, 13:00-14:00

Semantics Lunch (Computer Laboratory)

ABIs, linkers and other animals

UserStephen Kell, University of Cambridge.

HouseFW26.

ClockMonday 13 January 2014, 13:00-14:00

Semantics Lunch (Computer Laboratory)

POPL PC workshop

UserSpeaker to be confirmed.

HouseLT1.

ClockTuesday 01 October 2013, 09:30-17:00

Semantics Lunch (Computer Laboratory)

High-Level Separation Logic for Low-Level Code

UserNick Benton, MSR Cambridge.

HouseFW26.

ClockMonday 10 December 2012, 13:00-14:00

Semantics Lunch (Computer Laboratory)

Full Abstraction for PCF with Names

UserSteffen Lösch, University of Cambridge.

HouseFW26.

ClockMonday 26 November 2012, 13:00-14:00

Semantics Lunch (Computer Laboratory)

A Model-Learner Pattern for Bayesian Reasoning

UserAndy Gordon, Microsoft Research and University of Edinburgh.

HouseFW26.

ClockMonday 19 November 2012, 13:00-14:00

Semantics Lunch (Computer Laboratory)

Putting the thrill back into computing at school

UserSimon Peyton Jones, MSR Cambridge.

HouseFW26.

ClockMonday 12 November 2012, 13:00-14:00

Semantics Lunch (Computer Laboratory)

On distributed probabilistic strategies

UserGlynn Winskel.

HouseFW26.

ClockMonday 05 November 2012, 13:00-14:00

Semantics Lunch (Computer Laboratory)

The Power of Parameterization in Coinductive Proof

This will be the first Semantics Lunch of the term - please do come along (or email Peter.Sewell@cl.cam.ac.uk) with offers of talks.

UserChung-Kil Hur, MSR.

HouseFW26.

ClockMonday 22 October 2012, 13:00-14:00

Computer Laboratory Automated Reasoning Group Lunches

Semi-automatic Algorithm Synthesis (Case Study: Square Root)

UserMadalina Erascu - Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria.

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockThursday 21 June 2012, 13:00-14:00

Semantics Lunch (Computer Laboratory)

Ribbon Proofs for Separation Logic

UserJohn Wickerson.

HouseFW26.

ClockWednesday 20 June 2012, 13:30-13:45

Semantics Lunch (Computer Laboratory)

CerCo --- Certified Complexity

NB: Unusual day/time

UserDominic Mulligan (Bologna).

HouseFW26.

ClockThursday 31 May 2012, 11:00-12:00

Semantics Lunch (Computer Laboratory)

A Concurrent Logical Relation

NB: changed (again!) unusual day/time

UserJacob Thamsborg (ITU).

HouseFW26.

ClockWednesday 30 May 2012, 14:30-15:30

Semantics Lunch (Computer Laboratory)

Virtue of certified programming with decision procedures

NB: unusual day/time

UserVladimir Komendantsky (St Andrews).

HouseFW26.

ClockFriday 25 May 2012, 11:00-12:00

Semantics Lunch (Computer Laboratory)

From threads to events through classical program transformations

NB: Unusual day/time

UserGabriel Kerneis (PPS, Université Paris Diderot).

HouseFW26.

ClockWednesday 23 May 2012, 11:00-12:00

Semantics Lunch (Computer Laboratory)

Developing verified programs in Dafny

UserRustan Leino.

HouseFW26.

ClockMonday 27 February 2012, 12:45-14:00

Semantics Lunch (Computer Laboratory)

Understanding POWER Multiprocessors

UserSusmit Sarkar.

HouseFW26.

ClockMonday 14 November 2011, 12:45-14:00

Semantics Lunch (Computer Laboratory)

The Importance of Being Linearizable

UserAlexey Gotsman, IMDEA Software Institute.

HouseFW26.

ClockMonday 07 November 2011, 12:45-14:00

Semantics Lunch (Computer Laboratory)

Ribbon proofs for separation logic

UserJohn Wickerson.

HouseFW26.

ClockMonday 17 October 2011, 12:45-14:00

Semantics Lunch (Computer Laboratory)

Relating Two Semantics of Locally Scoped Names

Note unusual day, time and place: this will be in the ARG lunch slot

UserSteffen Lösch (University of Cambridge).

HouseRoom SS03, Computer Laboratory, William Gates Building.

ClockTuesday 30 August 2011, 13:00-14:00

Semantics Lunch (Computer Laboratory)

Composable Asynchronous Events/Formal Methods for Wireless Mesh Networks

Note unusual start time: talks at 12.50 prompt

UserSuresh Jagannathan/Peter Höfner.

HouseRoom FW26, Computer Laboratory, William Gates Building.

ClockMonday 23 May 2011, 12:45-14:00

Computer Laboratory Automated Reasoning Group Lunches

Mirage

UserAnil Madhavapeddy ( University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 16 November 2010, 13:00-14:00

Semantics Lunch (Computer Laboratory)

A Language for Mathematics

UserMohan Ganesalingam (University of Cambridge).

HouseRoom FW26, Computer Laboratory, William Gates Building.

ClockMonday 15 November 2010, 12:45-14:00

Semantics Lunch (Computer Laboratory)

Andrew Kennedy

POSTPONED - no Semantics Lunch meeting this week

UserAndrew Kennedy.

HouseRoom FW26, Computer Laboratory, William Gates Building.

ClockMonday 08 November 2010, 12:45-14:00

Semantics Lunch (Computer Laboratory)

Finding best paths in difficult conditions

(Change of speaker - this replaces Eric's talk)

UserAlex Gurney.

HouseRoom FW26, Computer Laboratory, William Gates Building.

ClockMonday 01 November 2010, 12:45-14:00

Semantics Lunch (Computer Laboratory)

Let should not be generalised

UserSimon Peyton Jones (Microsoft Research).

HouseRoom FW26, Computer Laboratory, William Gates Building.

ClockMonday 11 October 2010, 12:45-14:00

Semantics Lunch (Computer Laboratory)

Linear maps

UserDavid Walker (visiting from Princeton).

HouseRoom FW26, Computer Laboratory, William Gates Building.

ClockMonday 28 June 2010, 12:45-14:00

Computer Laboratory Automated Reasoning Group Lunches

Title to be confirmed

Canceled because of date clash with HCSS and workshop at MSR

UserSpeaker to be confirmed.

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 11 May 2010, 13:00-14:00

Computer Laboratory Automated Reasoning Group Lunches

Formal models of ARM processors in HOL

Presenters: Mike Gordon and Anthony Fox / This is a rehearsal of our HCSS talk on May 11

UserMike Gordon (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 04 May 2010, 13:00-14:00

Computer Laboratory Automated Reasoning Group Lunches

Verified just-in-time compiler on x86

Notice changed date

UserMagnus Myreen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 15 December 2009, 13:00-14:00

Semantics Lunch (Computer Laboratory)

Coarse-grained transactions

UserEric Koskinen (University of Cambridge).

HouseRoom FW26, Computer Laboratory, William Gates Building.

ClockMonday 30 November 2009, 12:45-14:00

Semantics Lunch (Computer Laboratory)

Completeness for algebraic theories of local state

UserSam Staton (Computer Laboratory, University of Cambridge).

HouseRoom FW26, Computer Laboratory, William Gates Building.

ClockMonday 16 November 2009, 12:45-14:00

Computer Laboratory Automated Reasoning Group Lunches

Abstract Threads

th orginally sheduled talk by Thomas Tuerk will probably be given next term

UserAlexander Malkis.

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 10 November 2009, 13:00-14:00

Computer Laboratory Automated Reasoning Group Lunches

Title to be confirmed

cancelled

UserEric Koskinen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 03 November 2009, 13:00-14:00

Semantics Lunch (Computer Laboratory)

Dependent types and program equivalence

UserStephanie Wierich, University of Pennsylvania.

HouseRoom FW26, Computer Laboratory, William Gates Building.

ClockMonday 02 November 2009, 12:45-14:00

Computer Laboratory Automated Reasoning Group Lunches

Title to be confirmed

Canceled

UserEric Koskinen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 09 June 2009, 13:00-14:00

Semantics Lunch (Computer Laboratory)

Segment logic (work in progress)

UserViktor Vafeiadis (Microsoft Research Cambridge).

HouseRoom FW26, Computer Laboratory, William Gates Building.

ClockMonday 23 March 2009, 12:45-14:00

Computer Laboratory Automated Reasoning Group Lunches

Semantics Lunch

Canceled, semantics lunch instead

UserSpeaker to be confirmed.

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 10 March 2009, 13:00-14:00

Semantics Lunch (Computer Laboratory)

Deny-guarantee reasoning

NOTE THE UNUSUAL DAY AND VENUE. This talk is in the ARG lunch slot.

UserMike Dodds (University of Cambridge).

HouseRoom SS03, Computer Laboratory, William Gates Building.

ClockTuesday 10 March 2009, 13:00-14:00

Semantics Lunch (Computer Laboratory)

Logics with Rank Operators

UserBjarki Holm (University of Cambridge).

HouseRoom FW26, Computer Laboratory, William Gates Building.

ClockMonday 23 February 2009, 12:45-14:00

Computer Laboratory Automated Reasoning Group Lunches

RGSep action inference

UserViktor Vafeiadis (Microsoft Research Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 17 February 2009, 13:00-14:00

Semantics Lunch (Computer Laboratory)

Semantics lunch organisational meeting

UserSpeaker to be confirmed.

HouseFW26.

ClockMonday 16 February 2009, 12:45-14:00

Computer Laboratory Automated Reasoning Group Lunches

Title to be confirmed

Canceled because of POPL

UserSpeaker to be confirmed.

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 20 January 2009, 13:00-14:00

Semantics Lunch (Computer Laboratory)

Secure Compilation of a Multi-Tier

UserIoannis Baltopoulos.

HouseFW26.

ClockMonday 08 December 2008, 12:45-14:00

Computer Laboratory Automated Reasoning Group Lunches

An ACL2 Tutorial

UserMatt Kaufmann (University of Texas at Austin).

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 02 December 2008, 13:00-14:00

Semantics Lunch (Computer Laboratory)

Title to be confirmed

UserJon Hayman.

HouseFW26.

ClockMonday 01 December 2008, 12:45-14:00

Semantics Lunch (Computer Laboratory)

Convergence of path-finding

UserAlex Gurney.

HouseFW26.

ClockMonday 24 November 2008, 12:45-14:00

Computer Laboratory Automated Reasoning Group Lunches

Mechanically verified LISP interpreters

Note unusual time

UserMagnus Myreen (University of Cambridge).

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 11 November 2008, 12:00-13:00

Semantics Lunch (Computer Laboratory)

Some notes on syntactic logical relations for pure System F

UserDimitrios Vytiniotis, MSR.

HouseFW26.

ClockMonday 10 November 2008, 12:45-14:00

Semantics Lunch (Computer Laboratory)

Deny-guarantee reasoning

UserMike Dodds (University of Cambridge).

HouseFW26.

ClockMonday 03 November 2008, 12:45-14:00

Semantics Lunch (Computer Laboratory)

Focusing on Pattern Matching

UserNeelakantan Krishnaswami, CMU.

HouseFW26.

ClockMonday 27 October 2008, 12:45-14:00

Semantics Lunch (Computer Laboratory)

An Invitation to Nominal Domain Theory

UserAndrew Pitts, Computer Lab.

HouseFW26.

ClockMonday 20 October 2008, 12:45-14:00

Computer Laboratory Automated Reasoning Group Lunches

A Constraint-Programming Framework For Bounded Program Verification

UserHelene Collavizza (Ecole Polytechnique Universitaire de Nice Sophia Antipolis).

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 11 March 2008, 13:00-14:00

Computer Laboratory Automated Reasoning Group Lunches

Automatic proof of SPARK verification conditions

UserPaul Jackson (School of Informatics, University of Edinburgh).

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 11 December 2007, 13:00-14:00

Computer Laboratory Automated Reasoning Group Lunches

One-pass Tableaux for Computation Tree Logic

Room changed

UserRajeev Goré (Australian National University).

HouseComputer Laboratory, William Gates Building, Room SS03.

ClockTuesday 07 August 2007, 13:00-14:00

Please see above for contact details for this list.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity