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.
Comparing higher-order encodings in logical frameworks and tile logic
BRUNI, ROBERTO;
2002-01-01
Abstract
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.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
