A Curry-Howard Correspondence for Event-Based Programming

Add to your list(s) Download to your calendar using vCal

• Neel Krishnaswami (University of Cambridge, formerly Birmingham)
• Friday 08 December 2017, 11:00-12:00
• Computer Science, The Sloman Lounge (UG).

If you have a question about this talk, please contact Paul Taylor.

Event-driven programming is based on a natural abstraction: an event is a computation that can eventually return a value. This talk shows how to exploit the intuition relating events and time by drawing a Curry- Howard correspondence between a functional event-driven programming language and a linear-time temporal logic. In this logic, the eventually proposition ◇A describes the type of events, and Girard’s linear logic describes the effectful and concurrent nature of the programs.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science, The Sloman Lounge (UG)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.