[Pl-seminar] 6/8 Seminar: Gabriel Scherer, Consistent Coercion Calculi and Reduction in the Face of Absurdity

[William J. Bowman]

NUPRL Seminar presents

Gabriel Scherer
INRIA in Paris-Rocquencourt

11:45am--1:15pm
Monday, June 8th, 2015
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)


Consistent Coercion Calculi, and Reduction in the Face of Absurdity

Abstract:
Consistent coercion calculi were recently (2010-2014) proposed by Julien
Crétin and Didier Rémy as an expressive framework to easily compose and
combine together various type-system features, notably subtyping and
polymorphism. Contrarily to most "all-encompassing type system
frameworks" out there, they enforce a very clear separation between the
program text, specifying the dynamic semantics, and the type information
present in derivations that does not influence the program execution.
They are also defined for full reduction, which makes them sound for any
reduction strategy (not just one of strict or lazy evaluation).

In later work (2015) with Didier Rémy, I extended consistent coercion
calculi with a form of "inconsistent abstraction" that allows to
abstract over logical assumptions that might be incorrect. To preserve
soundness, we have to block reduction around these assumptions,
resulting in a mix of full and weak reduction. This is necessary to
express some modern programming features, such as GADTs. There is then a
surprising coincidence, with a feature ("hiding") motivated by
programming language design that turns to be essential to get good
meta-theoretical properties (confluence).

In this talk, I hope to give a precise yet accessible presentation of
this brand of recent research. I will assume only basic knowledge of the
lambda-calculus and simple type systems, and give many examples to
motivate the general rules.


Bio:
Gabriel is a PhD student at INRIA in Paris-Rocquencourt, in the
"Gallium" team that focuses on programming languages design (OCaml,
Mezzo), type systems (inference via constraints, MLF), and correct tools
to manipulate programs (CompCert, Verasco). His Ph.D. work focuses on
using idea of proof theory and logic to answer programming language
questions. On the more practical side, he tries to contribute to the
OCaml programming language implementation, mostly as a reviewer of other
people's pull requests---maintaining and evolving an actively-used
programming language requires a lot of varied work.

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