|
1 @InProceedings{LeeCraryHarper07, |
|
2 author = {D.~K.~Lee and K.~Crary and R.~Harper}, |
|
3 title = {{T}owards a {M}echanized {M}etatheory of {Standard ML}}, |
|
4 booktitle = {Proc.~of the 34th POPL Symposium}, |
|
5 year = 2007, |
|
6 pages = {173--184} |
|
7 } |
|
8 |
|
9 @Unpublished{chargueraud09, |
|
10 author = "Arthur Chargu{\'e}raud", |
|
11 title = "{T}he {L}ocally {N}ameless {R}epresentation", |
|
12 year = "2009", |
|
13 note = "To appear in J.~of Automated Reasoning. |
|
14 {http://arthur.chargueraud.org/research/2009/ln/}", |
|
15 } |
|
16 |
|
17 @article{NaraschewskiNipkow99, |
|
18 author={W.~Naraschewski and T.~Nipkow}, |
|
19 title={{T}ype {I}nference {V}erified: {A}lgorithm {W} in {Isabelle/HOL}}, |
|
20 journal={J.~of Automated Reasoning}, |
|
21 year=1999, |
|
22 volume=23, |
|
23 pages={299--318}} |
|
24 |
1 @InProceedings{Berghofer99, |
25 @InProceedings{Berghofer99, |
2 author = {S.~Berghofer and M.~Wenzel}, |
26 author = {S.~Berghofer and M.~Wenzel}, |
3 title = {{I}nductive {D}atatypes in {HOL} - {L}essons {L}earned in |
27 title = {{I}nductive {D}atatypes in {HOL} - {L}essons {L}earned in |
4 {F}ormal-{L}ogic {E}ngineering}, |
28 {F}ormal-{L}ogic {E}ngineering}, |
5 booktitle = {Proc.~of the 12th TPHOLs conference}, |
29 booktitle = {Proc.~of the 12th TPHOLs conference}, |