Abstracts.2018.NbE.Mon&Sub

Normalization by evaluation for a monadic language with subtyping

by Carlos Tomé Cortiñas

Abstract

I will be giving a talk on using NbE (Normalization by Evaluation) to normalize terms in the STLC with base types extended with a subtyping relation and explicit coercions. Moreover, I will also take look at NbE in the context of STLC with a generic monad, i.e. a monad where we only assume return and bind but no specific operations.