equal
deleted
inserted
replaced
14 |
14 |
15 The difficulty can be appreciated by considering that the |
15 The difficulty can be appreciated by considering that the |
16 definition given by Leroy in [] is incorrect (it omits a |
16 definition given by Leroy in [] is incorrect (it omits a |
17 side-condition). |
17 side-condition). |
18 |
18 |
19 Examples: type-schemes |
19 Examples: type-schemes, Spi-calculus |
20 |
20 |
21 Contributions: We provide definitions for when terms |
21 Contributions: We provide definitions for when terms |
22 involving general bindings are alpha-equivelent. |
22 involving general bindings are alpha-equivelent. |
23 *} |
23 *} |
24 |
24 |
25 text {* A Brief Overview about the Nominal Logic Work *} |
25 section {* A Brief Overview about the Nominal Logic Work *} |
26 |
26 |
27 text {* Abstractions *} |
27 section {* Abstractions *} |
28 |
28 |
29 text {* Alpha-Equivalence and Free Variables *} |
29 section {* Alpha-Equivalence and Free Variables *} |
|
30 |
30 |
31 |
31 |
32 |
32 text {* |
33 text {* |
33 Acknowledgements: We thank Andrew Pitts for the many discussions |
34 Acknowledgements: We thank Andrew Pitts for the many discussions |
34 about the topic. We thank Peter Sewell for making [] available |
35 about the topic. We thank Peter Sewell for making [] available |