6 number = "4", |
6 number = "4", |
7 pages = "327--356", |
7 pages = "327--356", |
8 year = "2008" |
8 year = "2008" |
9 } |
9 } |
10 |
10 |
|
11 @InProceedings{norrish04, |
|
12 author = {M.~Norrish}, |
|
13 title = {{R}ecursive {F}unction {D}efinition for {T}ypes with {B}inders}, |
|
14 booktitle = {Proc.~of the 17th International Conference Theorem Proving in |
|
15 Higher Order Logics (TPHOLs)}, |
|
16 pages = {241--256}, |
|
17 year = {2004}, |
|
18 volume = {3223}, |
|
19 series = {LNCS} |
|
20 } |
|
21 |
11 @InProceedings{GunterOsbornPopescu09, |
22 @InProceedings{GunterOsbornPopescu09, |
12 author = {E.L.~Gunter and C.J.~Osborn and A.~Popescu}, |
23 author = {E.L.~Gunter and C.J.~Osborn and A.~Popescu}, |
13 title = {{T}heory {S}upport for {W}eak {H}igher {O}rder {A}bstract {S}yntax in |
24 title = {{T}heory {S}upport for {W}eak {H}igher {O}rder {A}bstract {S}yntax in |
14 {I}sabelle/{HOL}}, |
25 {I}sabelle/{HOL}}, |
15 booktitle = {Proc.~of the 4th International Workshop on Logical Frameworks and Meta-Languages: |
26 booktitle = {Proc.~of the 4th International Workshop on Logical Frameworks and Meta-Languages: |
16 Theory and Practice (LFMTP)}, |
27 Theory and Practice (LFMTP)}, |
17 pages = {12--20}, |
28 pages = {12--20}, |
18 year = {2009}, |
29 year = {2009}, |
|
30 series = {ENTCS} |
|
31 } |
|
32 |
|
33 @InProceedings{AydemirBohannonWeirich07, |
|
34 author = {B.~Aydemir and A.~Bohannon and S.~Weihrich}, |
|
35 title = {{N}ominal {R}easoning {T}echniques in {C}oq ({E}xtended {A}bstract)}, |
|
36 booktitle = {Proc.~of the 1st International Workshop on Logical Frameworks and Meta-Languages: |
|
37 Theory and Practice (LFMTP)}, |
|
38 pages = {69--77}, |
|
39 year = {2007}, |
19 series = {ENTCS} |
40 series = {ENTCS} |
20 } |
41 } |
21 |
42 |
22 @Unpublished{SatoPollack10, |
43 @Unpublished{SatoPollack10, |
23 author = {M.~Sato and R.~Pollack}, |
44 author = {M.~Sato and R.~Pollack}, |