Comparing Higher-order Encodings in Logical Frameworks and Tile Logic

Related