127 @BOOK{harrison-thesis, |
127 @BOOK{harrison-thesis, |
128 author = "John Harrison", |
128 author = "John Harrison", |
129 title = "Theorem Proving with the Real Numbers", |
129 title = "Theorem Proving with the Real Numbers", |
130 publisher = "Springer-Verlag", |
130 publisher = "Springer-Verlag", |
131 year = 1998} |
131 year = 1998} |
|
132 |
|
133 @BOOK{Barendregt81, |
|
134 AUTHOR = "H.~Barendregt", |
|
135 TITLE = "{T}he {L}ambda {C}alculus: {I}ts {S}yntax and {S}emantics", |
|
136 PUBLISHER = "North-Holland", |
|
137 YEAR = 1981, |
|
138 VOLUME = 103, |
|
139 SERIES = "Studies in Logic and the Foundations of Mathematics" |
|
140 } |
|
141 |
|
142 @BOOK{CurryFeys58, |
|
143 AUTHOR = "H.~B.~Curry and R.~Feys", |
|
144 TITLE = "{C}ombinatory {L}ogic", |
|
145 PUBLISHER = "North-Holland", |
|
146 YEAR = "1958", |
|
147 VOLUME = 1, |
|
148 SERIES = "Studies in Logic and the Foundations of Mathematics" |
|
149 } |
|
150 |
|
151 @Unpublished{UrbanKaliszyk11, |
|
152 author = {C.~Urban and C.~Kaliszyk}, |
|
153 title = {{G}eneral {B}indings and {A}lpha-{E}quivalence in {N}ominal {I}sabelle}, |
|
154 note = {submitted for publication}, |
|
155 month = {July}, |
|
156 year = {2010}, |
|
157 } |