Re: [TYPES] Example uses of impredicativity
"William J. Bowman" <wjb-r2/fXjr+/[email protected]>
| Newsgroups | gmane.comp.science.types |
|---|---|
| Message-ID | <[email protected]> |
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] Stefan, The type preserving CPS translation with answer type polymorphism requires impredicativity. Cédille uses impredicativity heavily, so that might be a better place to look than Coq. Although I guess that's more examples of (things like) Church encodings. (For that matter, the CPS translation is too.) -- Sent from my phoneamajig > On Jul 5, 2019, at 22:33, William J. Bowman <[email protected]> wrote: > > Stefan, > > The type preserving CPS translation with answer type polymorphism requires impredicativity.