Experiments in expressiveness of various styles of representation (primarily algebraic versus tagless final) in the contexts of interpretation, type checking, and theorem proving.
A motivation for these exercises is psygnisfive's basic-proof-development and assertion that tagless final is either useless for type checking or makes type checking impossible [personal communication].