Comparing Higher-Order Encodings in Logical Frameworks and Tile Logic
Roberto L. Bruni, Furio Honsell, Marina Lenisa, Marino Miculan · Electronic Notes in Theoretical Computer Science · 2002
In recent years, logical frameworks and tile logic have been separately proposed by our research groups, respectively in Udine and in Pisa, as suitable metalanguages with higher-order features for encoding and studying nominal calculi. This paper discusses the main features of the two approaches, tracing differences and analogies on the basis of two case studies: late π-calculus and lazy simply typed Λ-calculus.