CS Seminar, Jennifer Paykin (University of Pennsylvania, Wes '12): 'Logic, Categories, and Graphical user Interfaces'

Tuesday, April 21, 2015
4:15 PM - 5:30 PM (ET)
ESC 638
Event Type
Janet Burge, jburge@wesleyan.edu

Abstract: The Curry-Howard correspondence equates programming language type systems with mathematical logics. It has allowed researchers to formalize all sorts of interesting language features as type theories, including resource consciousness, control operators, and side effects. But combining such properties in a single language is not always straightforward.In this talk I will propose a unified framework for combining programming features that is based on adjunctions. An adjunction is an ubiquitous relationship between structures in category theory. In the extension of the Curry-Howard correspondence to category theory, it is only natural that adjunctions have an interpretation in type theory as a relationship between two type systems. In the second part of the talk we will explore graphical user interfaces as a concrete use case for our framework. Traditionally GUIs are made up of a collection of widgets (buttons, labels) and some functions, or callbacks, to be executed every time an event (mouse click, key press) occurs. We will explore a programming language that abstracts away first-class callbacks to make them more manageable. In doing so, we will identify which attributes we need such a language to have, and show how these properties fit into our feature framework.

Get Directions
Event Date
Event Time