[Pl-seminar] Reminder: Seminar TOMORROW: Gabriel Scherer, Deciding program equivalence with sums and the empty type

[Daniel Patterson]

Reminder that this is tomorrow, in 110 WVH.

On Mon, Nov 28, 2016 at 3:58 PM Daniel Patterson <dbp at ccs.neu.edu> wrote:
>
> NUPRL Seminar presents
>
> Gabriel Scherer
> Northeastern University
>
> 12:00-1:30pm
> Wednesday, December 7th, 2016
> Room 110 WVH (directions: http://www.ccs.neu.edu/home/wand/directions.html
> )
>
> Deciding program equivalence with sums and the empty type
>
> Abstract:
>
> The simply-typed λ-calculus, with only function types, is strongly
> normalizing, and its program equivalence relation is decidable: unlike in
> more advanced type system with polymorphism or effects, the natural
> "syntactic" equivalence (βη-equivalence) corresponds to natural "semantic"
> equivalence (observational or contextual equivalence), and is decidable.
> Adding product types (pairs) is easy and preserves these properties, but
> sums (disjoint unions) are, surprisingly, harder. It is only in 1995 that
> Neil Ghani proved that the equivalence in presence of sums is decidable,
> and the situation in presence of the empty type (zero-ary sum) was unknown.
>
> We propose an equivalence algorithm for sums and the empty type that takes
> inspiration from a proof-theoretic technique, named "focusing",designed for
> proof search. The exposition will be introductory; I will present the
> difficulties caused by sums and the empty type, present some of the
> existing approaches for sums in the literature, introduce focusing, and
> give a high-level intuition of our saturation-based algorithm and its
> termination argument. No previous knowledge of focusing is assumed. I
> expect some familiarity with typed lambda-calculi, but will recall all
> concepts used (for example, βη-equivalence) during the talk.
>
> Bio
>
> Gabriel is interested in theoretical aspects of type systems, programming
> language implementation, general programming language concepts, and even
> some syntactic aspects. He has a preference for the formalizable aspects,
> or formalizable approaches to programming language aspects, rather than the
> often subjective appeal to taste or intuition.
>
>
-------------- next part --------------
HTML attachment scrubbed and removed