Events and news relevant to the Laboratory for Foundations of Computer Science

[Ohad Kammar <ohad.kammar@ed.ac.uk>]

Quantitative Logic

Hi,

We'll have an LFCS seminar today:

  Thursday, 05 Jun, 11.10am

  Rasmus Møgelberg, IT University of Copenhagen

  This seminar is hybrid.

  

  Venue: Dugald Stewart Building 3.10 (Note unusual venue, day, and time)

  

  To attend remotely:

  URL: https://ed-ac-uk.zoom.us/j/88175309180

  Password: fKzEdb36

We're synchronising the seminar time with the teaching timetable, and

plan to start the talk at the advertised time, so please arrive a minute or two

earlier.

In detail:

----------------------------------------------------------------------

Rasmus Møgelberg, IT University of Copenhagen

https://studwww.itu.dk/~mogel/

  Thursday, 05 Jun, 11.10am

  Venue: Dugald Stewart Building 3.10 (Note unusual venue, day, and time)

  Remote participation:

  URL: https://ed-ac-uk.zoom.us/j/88175309180

  Password: fKzEdb36

Title: Induction and Recursion Principles in a Higher-Order Quantitative Logic

Abstract

Quantitative logic reasons about the degree to which

formulas are satisfied. This paper studies the fundamental

reasoning principles of higher-order quantitative logic and their

application to reasoning about probabilistic programs and

processes.

We construct an affine calculus for 1-bounded complete metric

spaces and the monad for probability measures equipped with

the Kantorovic distance. The calculus includes a form of guarded

recursion interpreted via Banach’s fixed point theorem, useful,

e.g., for recursive programming with processes. We then define an

affine higher-order quantitative logic for reasoning about terms

of our calculus. The logic includes novel principles for guarded

recursion, and induction over probability measures and natural

numbers.

Examples of reasoning in the logic include proofs of upper

bounds on distances of processes. We also show how our logic can

express coupling proofs —a powerful technique for comparing

probabilistic processes.

The talk is based on joint work with Giorgio Bacci.

----------------------------------------------------------------------

Upcoming seminars:

------------------

17 Jun: Andreas Abel, Gothenburg University / Chalmers

26 Jun: John Longley, Lecture 1, University of Edinburgh

27 Jun: John Longley, Lecture 2, University of Edinburgh

01 Jul: John Longley, Lecture 3, University of Edinburgh

08 Jul: John Longley, Lecture 4, University of Edinburgh

05 Aug: Michael Sperber, Active Group GmbH

If you would like to propose a speaker, or speak yourself, please contact me.

The seminar webpages:

http://web.inf.ed.ac.uk/lfcs/events/lfcs-seminars

Yours,

Ohad.

The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.