by Jon Sterling
An introduction to the theme of the workshop, the marriage of structural and behavioral approaches to understanding programming languages and mathematics.
What's the meaning behind the PL slogan, 'computation is continuous'? In order to find out, we'll explore the basics of a field called domain theory. Domain theory is interesting because it lets us characterize continuity with a very simple property. This version of continuity, though, is abstract enough that it's applicable to how we think about programs!
From there we'll see how we can use this simple slogan to apply all the tools of normal mathematics to study problems around systems like the lambda calculus and dip our toes into the wonderful world of denotational semantics.
This talk assumes as few mathematical prerequisites as possible, though its content is a little mathematical. It would be helpful if participants were familiar with the lambda calculus, or a functional language based on it.
The concept of free structure on signatures or graphs is well known in both category theory and type theory. What is not as well known in type theory is how to generalize this concept of free structure to more exotic scenarios involving hypergraphs in higher dimensions. In this talk I will explain first why this is even an interesting problem for higher dimensional type theories. Next I will discuss how computads, operads, and higher dimensional polytopic sets provide important insights. Finally I will present some concrete applications and demos.
In this talk, I present the current state of a new research project: applying a Curry-style extensional type theory to an existing programming language, namely Racket. I'll demonstrate the state of the theory and implementation and talk about current challenges.
by Jon Sterling