1 

     1 

     2 @Unpublished{Traytel12,

     2 @Unpublished{Traytel12,

     3   author =       {D.~Traytel and A.~Popescu and J.~C.~Blanchette},

     3   author =       {D.~Traytel and A.~Popescu and J.~C.~Blanchette},

     4   title =        {{F}oundational, {C}ompositional ({C}o)datatypes for {H}igher-{O}rder 

     4   title =        {{F}oundational, {C}ompositional ({C}o)datatypes for {H}igher-{O}rder 

     5                   {L}ogic: {C}ategory {T}heory {A}pplied to {T}heorem {P}roving},

     5                   {L}ogic: {C}ategory {T}heory {A}pplied to {T}heorem {P}roving},

     7   year =         {2012}

     7   year =         {2012}

     8 }

     8 }

     9 

     9 

    10 @inproceedings{pfenningsystem,

    10 @inproceedings{pfenningsystem,

    11   author =       "F.~Pfenning and C.~Sch{\"u}rmann", 

    11   author =       "F.~Pfenning and C.~Sch{\"u}rmann", 

    40 

    40 

    41 @InProceedings{WeirichYorgeySheard11,

    41 @InProceedings{WeirichYorgeySheard11,

    42   author = 	 {S.~Weirich and B.~Yorgey and T.~Sheard},

    42   author = 	 {S.~Weirich and B.~Yorgey and T.~Sheard},

    43   title = 	 {{B}inders {U}nbound},

    43   title = 	 {{B}inders {U}nbound},

    44   booktitle = 	 {Proc.~of the 16th International Conference on Functional Programming (ICFP)},

    44   booktitle = 	 {Proc.~of the 16th International Conference on Functional Programming (ICFP)},

    46 }

    47 }

    47 

    48 

    48 @InProceedings{UrbanKaliszyk11,

    49 @InProceedings{UrbanKaliszyk11,

    49   author =       {C.~Urban and C.~Kaliszyk},

    50   author =       {C.~Urban and C.~Kaliszyk},

    50   title =        {{G}eneral {B}indings and {A}lpha-{E}quivalence in {N}ominal {I}sabelle},

    51   title =        {{G}eneral {B}indings and {A}lpha-{E}quivalence in {N}ominal {I}sabelle},