ICE-TCS seminar: Denis Firsov

Generic derivation of induction for impredicative encodings in Cedille

  • 23.2.2018, 12:10 - 13:00

ICE-TCS-logo-200px

Date and time: Friday, 23 February 2018 from 12:10 till 13:00
Place: M110 at Reykjavik University

Title: Generic derivation of induction for impredicative encodings in Cedille

Speaker: Denis Firsov (The University of Iowa, Iowa City, USA)

Abstract

This talk presents generic derivations of induction for impredicatively typed lambda-encoded datatypes, in the Cedille type theory.

Cedille is a pure type theory extending the Curry-style Calculus of Constructions with implicit products, primitive heterogeneous equality, and dependent intersections. All data erase to pure lambda terms, and there is no built-in notion of datatype.

The derivations are generic in the sense that we derive induction for any datatype which arises as the least fixed point of a signature functor. We consider Church-style and Mendler-style lambda-encodings. Moreover, the isomorphism of these encodings is proved. Also, we formalize Lambek's lemma as a consequence of expected laws of cancellation, reflection, and fusion.

This is joint work with Aaron Stump.