equal
deleted
inserted
replaced
7 year = {2005}, |
7 year = {2005}, |
8 volume = {3603}, |
8 volume = {3603}, |
9 series = {LNCS} |
9 series = {LNCS} |
10 } |
10 } |
11 |
11 |
|
12 @INPROCEEDINGS{Pottier06, |
|
13 author = {F.~Pottier}, |
|
14 title = {{A}n {O}verview of {C$\alpha$ml}}, |
|
15 year = {2006}, |
|
16 booktitle = {ACM Workshop on ML}, |
|
17 pages = {27--52}, |
|
18 volume = {148}, |
|
19 number = {2}, |
|
20 series = {ENTCS} |
|
21 } |
12 |
22 |
13 @Unpublished{HuffmanUrban10, |
23 @Unpublished{HuffmanUrban10, |
14 author = {B.~Huffman and C.~Urban}, |
24 author = {B.~Huffman and C.~Urban}, |
15 title = {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle}, |
25 title = {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle}, |
16 note = {To appear at ITP 2010}, |
26 note = {To appear at ITP 2010}, |
28 |
38 |
29 @Unpublished{SewellBestiary, |
39 @Unpublished{SewellBestiary, |
30 author = {P.~Sewell}, |
40 author = {P.~Sewell}, |
31 title = {{A} {B}inding {B}estiary}, |
41 title = {{A} {B}inding {B}estiary}, |
32 note = {Personal communication.} |
42 note = {Personal communication.} |
|
43 } |
|
44 |
|
45 @InProceedings{challenge05, |
|
46 author = {B.~E.~Aydemir and A.~Bohannon and M.~Fairbairn and |
|
47 J.~N.~Foster and B.~C.~Pierce and P.~Sewell and |
|
48 D.~Vytiniotis and G.~Washburn and S.~Weirich and |
|
49 S.~Zdancewic}, |
|
50 title = {{M}echanized {M}etatheory for the {M}asses: {T}he \mbox{Popl}{M}ark |
|
51 {C}hallenge}, |
|
52 booktitle = {Proc.~of the 18th International Conference on Theorem Proving in Higher-Order |
|
53 Logics (TPHOLs)}, |
|
54 pages = {50--65}, |
|
55 year = {2005}, |
|
56 volume = {3603}, |
|
57 series = {LNCS} |
33 } |
58 } |
34 |
59 |
35 @Unpublished{SatoPollack10, |
60 @Unpublished{SatoPollack10, |
36 author = {M.~Sato and R.~Pollack}, |
61 author = {M.~Sato and R.~Pollack}, |
37 title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus}, |
62 title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus}, |