On the role of names in reasoning about lambda-tree syntax specifications
Lambda tree syntax (a variant of HOAS) and nominal techniques are two approaches to representing and reasoning about languages containing bindings. Although they are based on separate foundations, recent advances in the proof theory of generic judgments have shown that one may be able to incorporate some aspects of nominal techniques (i.e., the equivariant principle) to simplify reasoning about λ-tree syntax specifications, while still maintaining the crucial aspects of λ-tree syntax. In this...[Show more]
|Collections||ANU Research Publications|
|Source:||Electronic Notes in Theoretical Computer Science|
|01_Tiu_On_the_role_of_names_in_2009.pdf||248.72 kB||Adobe PDF||Request a copy|
|02_Tiu_On_the_role_of_names_in_2009.pdf||163.63 kB||Adobe PDF||Request a copy|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.