Type theories can be formalized using the intrinsically (hard) or theextrinsically (soft) typed style . In large libraries of type theoreticalfeatures, often both styles are present, which can lead to code duplication and integration issues . We define an operator that systematically translates a hard-typed into thecorresponding soft-typing formulation . We implement our operator in the MMT system and apply it to a library oftype-theoretical features .

Author(s) : Florian Rabe, Navid Roux

Links : PDF - Abstract

Code :

Keywords : type - operator - hard - soft - typed -

Leave a Reply

Your email address will not be published. Required fields are marked *