|
1 @InProceedings{GunterOsbornPopescu09, |
|
2 author = {E.L.~Gunter and C.J.~Osborn and A.~Popescu}, |
|
3 title = {{T}heory {S}upport for {W}eak {H}igher {O}rder {A}bstract {S}yntax in |
|
4 {I}sabelle/{HOL}}, |
|
5 booktitle = {Proc.~of the 4th International Workshop on Logical Frameworks and Meta-Languages: |
|
6 Theory and Practice (LFMTP)}, |
|
7 pages = {12--20}, |
|
8 year = {2009}, |
|
9 series = {ENTCS} |
|
10 } |
|
11 |
|
12 @Unpublished{SatoPollack10, |
|
13 author = {M.~Sato and R.~Pollack}, |
|
14 title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus}, |
|
15 note = {To appear in {\it Journal of Symbolic Computation}} |
|
16 } |
|
17 |
|
18 @article{GabbayPitts02, |
|
19 author = {M.~J.~Gabbay and A.~M.~Pitts}, |
|
20 title = {{A} {N}ew {A}pproach to {A}bstract {S}yntax with {V}ariable |
|
21 {B}inding}, |
|
22 journal = {Formal Aspects of Computing}, |
|
23 volume = {13}, |
|
24 year = 2002, |
|
25 pages = {341--363} |
|
26 } |
|
27 |
|
28 @article{Pitts03, |
|
29 author = {A.~M.~Pitts}, |
|
30 title = {{N}ominal {L}ogic, {A} {F}irst {O}rder {T}heory of {N}ames and |
|
31 {B}inding}, |
|
32 journal = {Information and Computation}, |
|
33 year = {2003}, |
|
34 volume = {183}, |
|
35 pages = {165--193} |
|
36 } |
|
37 |
|
38 @InProceedings{BengtsonParrow07, |
|
39 author = {J.~Bengtson and J.~Parrow}, |
|
40 title = {Formalising the pi-{C}alculus using {N}ominal {L}ogic}, |
|
41 booktitle = {Proc.~of the 10th International Conference on |
|
42 Foundations of Software Science and Computation Structures (FOSSACS)}, |
|
43 year = 2007, |
|
44 pages = {63--77}, |
|
45 series = {LNCS}, |
|
46 volume = {4423} |
|
47 } |
|
48 |
|
49 @inproceedings{BengtsonParow09, |
|
50 author = {J.~Bengtson and J.~Parrow}, |
|
51 title = {{P}si-{C}alculi in {I}sabelle}, |
|
52 booktitle = {Proc of the 22nd Conference on Theorem Proving in |
|
53 Higher Order Logics (TPHOLs)}, |
|
54 year = 2009, |
|
55 pages = {99--114}, |
|
56 series = {LNCS}, |
|
57 volume = {5674} |
|
58 } |
|
59 |
|
60 @inproceedings{TobinHochstadtFelleisen08, |
|
61 author = {S.~Tobin-Hochstadt and M.~Felleisen}, |
|
62 booktitle = {Proc.~of the 35rd Symposium on |
|
63 Principles of Programming Languages (POPL)}, |
|
64 title = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme}, |
|
65 publisher = {ACM}, |
|
66 year = {2008}, |
|
67 pages = {395--406} |
|
68 } |
|
69 |
|
70 @InProceedings{UrbanCheneyBerghofer08, |
|
71 author = "C.~Urban and J.~Cheney and S.~Berghofer", |
|
72 title = "{M}echanizing the {M}etatheory of {LF}", |
|
73 pages = "45--56", |
|
74 year = 2008, |
|
75 booktitle = "Proc.~of the 23rd IEEE Symposium on Logic in Computer Science (LICS)" |
|
76 } |
|
77 |
|
78 @InProceedings{UrbanZhu08, |
|
79 title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof", |
|
80 author = "C.~Urban and B.~Zhu", |
|
81 booktitle = "Proc.~of the 9th International Conference on Rewriting Techniques |
|
82 and Applications (RTA)", |
|
83 year = "2008", |
|
84 pages = "409--424", |
|
85 series = "LNCS", |
|
86 volume = 5117 |
|
87 } |
|
88 |
|
89 @Article{UrbanPittsGabbay04, |
|
90 title = "{N}ominal {U}nification", |
|
91 author = "C.~Urban and A.M.~Pitts and M.J.~Gabbay", |
|
92 journal = "Theoretical Computer Science", |
|
93 pages = "473--497", |
|
94 volume = "323", |
|
95 number = "1-3", |
|
96 year = "2004" |
|
97 } |
|
98 |
|
99 @Article{Church40, |
|
100 author = {A.~Church}, |
|
101 title = {{A} {F}ormulation of the {S}imple {T}heory of {T}ypes}, |
|
102 journal = {Journal of Symbolic Logic}, |
|
103 year = {1940}, |
|
104 volume = {5}, |
|
105 number = {2}, |
|
106 pages = {56--68} |
|
107 } |
|
108 |
|
109 |
|
110 @Manual{PittsHOL4, |
|
111 title = {{S}yntax and {S}emantics}, |
|
112 author = {A.~M.~Pitts}, |
|
113 note = {Part of the documentation for the HOL4 system.} |
|
114 } |
|
115 |
|
116 |
|
117 @book{PaulsonBenzmueller, |
|
118 year={2009}, |
|
119 author={Benzm{\"u}ller, Christoph and Paulson, Lawrence C.}, |
|
120 title={Quantified Multimodal Logics in Simple Type Theory}, |
|
121 note={{http://arxiv.org/abs/0905.2435}}, |
|
122 series={{SEKI Report SR--2009--02 (ISSN 1437-4447)}}, |
|
123 publisher={{SEKI Publications}} |
|
124 } |
|
125 |
|
126 @Article{Cheney06, |
|
127 author = {J.~Cheney}, |
|
128 title = {{C}ompleteness and {H}erbrand {T}heorems for {N}ominal {L}ogic}, |
|
129 journal = {Journal of Symbolic Logic}, |
|
130 year = {2006}, |
|
131 volume = {71}, |
|
132 number = {1}, |
|
133 pages = {299--320} |
|
134 } |
|
135 |