Tuesday, July 11, 2017 - 3:30pm to 4:30pm
Location:Blelloch-Skees Conference Room 8115 Gates Hillman Centers
Speaker:GABRIEL SCHERER, Post-Doctoral Researcher http://www.ccis.northeastern.edu/people/gabriel-scherer/
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.—Gabriel Scherer ("gasche") is a post-doctoral researcher at Northeastern University, Boston, working with Amal Ahmed on formal aspects multi-language programming systems.