Comparing higher-order encodings in logical frameworks and tile logic
| Author(s) : | Marino Miculan B B Marina Lenisa A Furio Honsell Roberto Bruni, |
| Publisher : | N/A |
| Publication Date : | 2001 |
| ISSN : | N/A |
| Abstract : | 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 ss-calculus and lazy simply typed *-calculus., |