[Pl-seminar] Surprise PL Seminar! TOMORROW, 1:30pm, 366 WVH: Which simple types have a unique inhabitant?

[William J. Bowman]

Some of us were asking about Gabriel's ICFP work, so he decided to give us a talk, so:

NUPRL Seminar presents

Gabriel Scherer
INRIA in Paris-Rocquencourt

1:30pm--2:30pm
Thursday, June 11th, 2015
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Which simple types have a unique inhabitant?

Abstract:
In this talk I will present an algorithm that takes a type of the simply-typed
lambda-calculus with sums, and says that:

(0) it is not inhabited, or
(1) it is uniquely inhabited (and gives the unique program at this type), or
(2) it is not uniquely inhabited (and gives two distinct programs at this type).

The algorithm relies on a novel "saturating" variant of focused
intuitionistic logic, which is very close to the existing notion of
maximal multi-focusing. (I will introduce focusing in this talk, no
previous knowledge of it is assumed.) Making the algorithm terminating
relies on techniques of propositional proof search, that needed to be
adapted to preserve computational correctness: if you cut the search
space too harshly, you may claim a type is uniquely inhabited when it
is not.


Bio:
Gabriel, who last spoke to us on Monday, 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: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: Digital signature
URL: <http://lists.ccs.neu.edu/pipermail/pl-seminar/attachments/20150610/458ec03e/attachment.pgp>