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 $\pi$-calculus and lazy simply
typed $\lambda$-calculus.