159 title = {Tutorial to Locales and Locale Interpretation}, |
159 title = {Tutorial to Locales and Locale Interpretation}, |
160 institution = TUM, |
160 institution = TUM, |
161 note = {\url{http://isabelle.in.tum.de/doc/locales.pdf}} |
161 note = {\url{http://isabelle.in.tum.de/doc/locales.pdf}} |
162 } |
162 } |
163 |
163 |
164 @article{Ballarin2013, |
164 @article{Ballarin2014, |
165 author = {Ballarin, Clemens}, |
165 author = {Ballarin, Clemens}, |
166 journal = JAR, |
166 journal = JAR, |
167 note = {Online version; to appear in print.}, |
|
168 publisher = Springer, |
167 publisher = Springer, |
169 title = {Locales: A Module System for Mathematical Theories}, |
168 title = {Locales: A Module System for Mathematical Theories}, |
|
169 volume = 52, |
|
170 number = 2, |
|
171 pages = {123--153}, |
170 url = {http://dx.doi.org/10.1007/s10817-013-9284-7}, |
172 url = {http://dx.doi.org/10.1007/s10817-013-9284-7}, |
171 year = {2013}} |
173 year = {2014}} |
172 |
174 |
173 @InCollection{Barendregt-Geuvers:2001, |
175 @InCollection{Barendregt-Geuvers:2001, |
174 author = {H. Barendregt and H. Geuvers}, |
176 author = {H. Barendregt and H. Geuvers}, |
175 title = {Proof Assistants using Dependent Type Systems}, |
177 title = {Proof Assistants using Dependent Type Systems}, |
176 booktitle = {Handbook of Automated Reasoning}, |
178 booktitle = {Handbook of Automated Reasoning}, |