Date/Time
Date(s) - 13/08/2015
3:00 pm - 4:30 pm
Location
Computer and Information Sciences
Professor Jeremy Siek from Indiana University, Bloomington will be giving a talk on : “The Polymorphic Blame Calculus and Parametricity” at the University of Strathclyde on 13 August at 3.00pm.
Abstract:
The Polymorphic Blame Calculus (PBC) of Ahmed et al. (2011) combines polymorphism, as in System F, with type dynamic and runtime casts, as in the Blame Calculus. The PBC is carefully designed to ensure
relational parametricity, that is, to ensure that type abstractions do not reveal their abstracted types. The operational semantics of PBC uses runtime sealing and syntactic barriers to enforce parametricity. However, it is an open question as to whether these mechanisms actually guarantee parametricity for the PBC. Furthermore, there is some question regarding what parametricity means in the context of the PBC, as we have examples that are morally parametric but not technically so. This talk will review the design of the PBC with respect to ensuring parametricity and hopefully start a discussion regarding what parametricity should mean for the PBC
Bio:
Jeremy Siek is an Associate Professor at Indiana University Bloomington. Jeremy’s areas of research include programming language design, type systems, mechanized theorem proving using proof assistants, and optimizing compilers. Jeremy’s Ph.D. thesis explored foundations for constrained templates, aka the “concepts” proposal for C++. Prior to that, Jeremy developed the Boost Graph Library, a C++ generic library for graph algorithms and data structures. Jeremy post-doc’d at Rice University where he developed the idea of gradual typing: a type system that integrates both dynamic and static typing in the same programming language. Jeremy is currently working on several open questions regarding gradual typing. Is the polymorphic blame calculus really parametric? How should gradual typing be combined with other features such as dependent types? What is the formal criteria for gradually typed languages? Is it possible to create a high-performance implementation of a gradually-typed languages? In 2009 Jeremy received the NSF CAREER award to fund his project: “Bridging the Gap Between Prototyping and Production”. In 2010 and again in 2015, Jeremy was awarded a Distinguished Visiting Fellowship from the Scottish Informatics & Computer Science Alliance.
Please contact Professor Neil Ghani for more information
