Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS seminar: Neelakantan (Neel) Krishnaswami: Curry-Howard for GUIs via Linear Temporal Classical Linear Logic

LFCS seminar: Neelakantan (Neel) Krishnaswami: Curry-Howard for GUIs via Linear Temporal Classical Linear Logic

— filed under:

What
  • LFCS Seminar
When May 19, 2015
from 04:00 PM to 05:00 PM
Add event to calendar vCal
iCal

Abstract:

 

Modern graphical user interface are structured with an event-driven

architecture: programmers write programs as a collection of small

imperative callbacks, which are invoked by an event loop as program

events occur. That is, they must write higher-order imperative programs

in continuation-passing style, which is notoriously challenging.

 

Using ideas from realizability theory, it is possible to build a model

of classical linear logic on top of an event-based architecture. Since

classical linear logic has a proof theory in terms of process calculi,

we gain a neat explanation of why programmers talk about GUI programs in

terms of concurrency, even though they implement them in terms of state

and control. Furthermore, we now also have a type structure upon which

 

we can build powerful abstractions -- historically the bane of UI toolkits.

Document Actions