PRL Seminars

During the past year, I have devoted part of my time to enhancing the Nuprl programming environment. My final goal is to describe formal abstract data types, but in the process I have had to add several new types and definitions to the type theory.

I will desribe my work with "squiggle equality," which is a type that denotes congruence between two terms, and provides a solution to the well-known `(x + 1) - 1 = x' problem. I will also describe the intersection type and the very-dependent function type, as well as some programming constructs such as pattern-matching.

All of these are tools that I am using to describe formal abstract data types, which I cover if I have time.