[Pl-seminar] Reminder: Seminar Tomorrow: Noam Zeilberger, A Categorical Perspective on Type Refinement

William J. Bowman wilbowma at ccs.neu.edu
Tue Jul 12 12:51:57 EDT 2016


Reminder: Talk tomorrow!

On Fri, Jul 08, 2016 at 01:41:00PM -0400, William J. Bowman wrote:
> 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



> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar

-------------- 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/20160712/7e7f3db2/attachment.pgp>


More information about the pl-seminar mailing list