[Pl-seminar] 7/13 Seminar: Noam Zeilberger, A Categorical Perspective on Type Refinement

[William J. Bowman]

NUPRL Seminar presents

Noam Zeilberger
Inria Ecole Polytechnique

11:45am
Wednesday July 13, 2016
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)


A Categorical Perspective on Type Refinement

Abstract:
A "type refinement system" is a type system built on top of
a typed programming language, as an extra layer of typing.  Over the
past few years Paul-André Melliès and I have investigated a
categorical foundation for type refinement systems, which is based on
the idea of looking at a type refinement system "backwards", in terms
of the functor which erases the extra layer of types.  The talk will
give an introduction to this framework as well as to some of the
insights that it offers, such as:

* The idea of viewing Hoare logic as a type refinement system.
* The importance of the bifibrational operations of "pushing forward" and
"pulling back" (which generalize strongest postconditions and weakest
preconditions).
* How those operations can be combined with a monoidal closed structure, to
model type refinement systems built over pure lambda calculus.

I will not assume any prior background in category theory, although as
background reading audience members may be interested in the lecture
notes for my recent course at OPLSS
(http://noamz.org/oplss16/refinements-notes.pdf, especially Ch.3).


Bio:
Since receiving his PhD from Carnegie Mellon in 2009, Noam Zeilberger
has been actively pursuing a career as an itinerant postdoc, with gigs
in Paris (Laboratoire PPS), Madrid (IMDEA Software), Princeton (IAS),
and back in Paris (MSR-Inria).  He is currently a member of Inria Team
Parsifal at Ecole Polytechnique.  In his free time, he enjoys
enumerating lambda terms, and his favorite combinators are B, C and I.

-- 
William J. Bowman
Northeastern University
College of Computer and Information Science
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: not available
URL: <http://lists.ccs.neu.edu/pipermail/pl-seminar/attachments/20160708/7b5129fa/attachment.pgp>