|
754
|
1 |
(*<*)
|
|
|
2 |
theory Paper
|
|
1473
|
3 |
imports "../Nominal/Test"
|
|
754
|
4 |
begin
|
|
|
5 |
(*>*)
|
|
|
6 |
|
|
|
7 |
section {* Introduction *}
|
|
|
8 |
|
|
|
9 |
text {*
|
|
1485
|
10 |
|
|
|
11 |
It has not yet fared so well in the POPLmark challenge
|
|
|
12 |
as the second part contain a formalisation of records
|
|
|
13 |
where ...
|
|
|
14 |
|
|
|
15 |
The difficulty can be appreciated by considering that the
|
|
|
16 |
definition given by Leroy in [] is incorrect (it omits a
|
|
|
17 |
side-condition).
|
|
|
18 |
|
|
|
19 |
Examples: type-schemes
|
|
|
20 |
|
|
|
21 |
Contributions: We provide definitions for when terms
|
|
|
22 |
involving general bindings are alpha-equivelent.
|
|
|
23 |
*}
|
|
|
24 |
|
|
|
25 |
text {* A Brief Overview about the Nominal Logic Work *}
|
|
|
26 |
|
|
|
27 |
text {* Abstractions *}
|
|
|
28 |
|
|
|
29 |
text {* Alpha-Equivalence and Free Variables *}
|
|
|
30 |
|
|
|
31 |
|
|
|
32 |
text {*
|
|
|
33 |
Acknowledgements: We thank Andrew Pitts for the many discussions
|
|
|
34 |
about the topic. We thank Peter Sewell for making [] available
|
|
|
35 |
to us and explaining some of the finer points of the OTT tool.
|
|
|
36 |
|
|
754
|
37 |
|
|
|
38 |
*}
|
|
|
39 |
|
|
1484
|
40 |
|
|
|
41 |
|
|
754
|
42 |
(*<*)
|
|
|
43 |
end
|
|
|
44 |
(*>*) |