author | ballarin |
Thu, 15 Oct 2009 22:07:18 +0200 | |
changeset 32981 | 0114e04a0d64 |
parent 27063 | d1d35284542f |
child 32983 | a6914429005b |
permissions | -rw-r--r-- |
27063 | 1 |
@unpublished{IsarRef, |
2 |
author = "Markus Wenzel", |
|
3 |
title = "The {Isabelle/Isar} Reference Manual", |
|
4 |
note = "Part of the Isabelle distribution, \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}." |
|
14586 | 5 |
} |
6 |
||
27063 | 7 |
@book {Jacobson1985, |
8 |
author = "Nathan Jacobson", |
|
9 |
title = "Basic Algebra", |
|
10 |
volume = "I", |
|
11 |
publisher = "Freeman", |
|
12 |
edition = "2nd", |
|
13 |
year = 1985, |
|
14586 | 14 |
available = { CB } |
15 |
} |
|
16 |
||
27063 | 17 |
% TYPES 2006 |
14586 | 18 |
|
27063 | 19 |
@inproceedings{HaftmannWenzel2007, |
20 |
author = "Florian Haftmann and Makarius Wenzel", |
|
21 |
title = "Constructive Type Classes in {Isabelle}", |
|
22 |
pages = "160--174", |
|
23 |
crossref = "AltenkirchMcBride2007", |
|
14586 | 24 |
available = { CB } |
25 |
} |
|
26 |
||
27063 | 27 |
@proceedings{AltenkirchMcBride2007, |
28 |
editor = "Thorsten Altenkirch and Connor McBride", |
|
29 |
title = "Types for Proofs and Programs, TYPES 2006, Nottingham, UK", |
|
30 |
booktitle = "Types for Proofs and Programs, TYPES 2006, Nottingham, UK", |
|
14586 | 31 |
publisher = "Springer", |
27063 | 32 |
series = "LNCS 4502", |
33 |
year = 2007 |
|
14586 | 34 |
} |
35 |
||
36 |
||
27063 | 37 |
@techreport{Ballarin2006a, |
38 |
author = "Clemens Ballarin", |
|
39 |
title = "Interpretation of Locales in {Isabelle}: Managing Dependencies between Locales", |
|
40 |
institution = "Technische Universit{\"a}t M{\"u}nchen", |
|
41 |
number = "TUM-I0607", |
|
42 |
year = 2006 |
|
14586 | 43 |
} |
44 |
||
32981 | 45 |
% TYPES 2008 |
46 |
||
47 |
@inproceedings{HaftmannWenzel2009, |
|
48 |
author = "Florian Haftmann and Makarius Wenzel", |
|
49 |
title = "Local theory specifications in {Isabelle}/{Isar}", |
|
50 |
pages = "153--168", |
|
51 |
crossref = "BerardiEtAl2009" |
|
52 |
} |
|
53 |
||
54 |
@proceedings{BerardiEtAl2009, |
|
55 |
editor = "Stefano Berardi and Ferruccio Damiani and Ugo de Liguoro", |
|
56 |
title = "Types for Proofs and Programs, TYPES 2008, Torino, Italy", |
|
57 |
booktitle = "Types for Proofs and Programs, TYPES 2008, Torino, Italy", |
|
58 |
series = "LNCS 5497", |
|
59 |
publisher = "Springer", |
|
60 |
year = 2009 |
|
61 |
} |
|
62 |
||
27063 | 63 |
% MKM 2006 |
64 |
||
65 |
@inproceedings{Ballarin2006b, |
|
66 |
author = "Clemens Ballarin", |
|
67 |
title = "Interpretation of Locales in {Isabelle}: Theories and Proof Contexts", |
|
68 |
pages = "31--43", |
|
69 |
crossref = "BorweinFarmer2006" |
|
14586 | 70 |
} |
71 |
||
27063 | 72 |
@proceedings{BorweinFarmer2006, |
73 |
editor = "Jonathan M. Borwein and William M. Farmer", |
|
74 |
title = "Mathematical knowledge management, MKM 2006, Wokingham, UK", |
|
75 |
booktitle = "Mathematical knowledge management, MKM 2006, Wokingham, UK", |
|
76 |
series = "LNCS 4108", |
|
77 |
publisher = "Springer", |
|
78 |
year = 2006, |
|
14586 | 79 |
available = { CB } |
80 |
} |
|
81 |
||
27063 | 82 |
% TPHOLs 1999 |
14586 | 83 |
|
27063 | 84 |
@inproceedings{KammullerEtAl1999, |
85 |
author = "Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson", |
|
86 |
title = "Locales: A Sectioning Concept for {Isabelle}", |
|
87 |
pages = "149--165", |
|
88 |
crossref = "BertotEtAl1999", |
|
89 |
available = { CB } |
|
14586 | 90 |
} |
91 |
||
27063 | 92 |
@book{BertotEtAl1999, |
93 |
editor = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th{\'e}ry", |
|
94 |
title = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France", |
|
95 |
booktitle = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France", |
|
96 |
publisher = "Springer", |
|
97 |
series = "LNCS 1690", |
|
98 |
year = 1999 |
|
16168
adb83939177f
Locales: new element constrains, parameter renaming with syntax,
ballarin
parents:
14586
diff
changeset
|
99 |
} |