@InProceedings{GunterOsbornPopescu09, author = {E.L.~Gunter and C.J.~Osborn and A.~Popescu}, title = {{T}heory {S}upport for {W}eak {H}igher {O}rder {A}bstract {S}yntax in {I}sabelle/{HOL}}, booktitle = {Proc.~of the 4th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)}, pages = {12--20}, year = {2009}, series = {ENTCS}}@Unpublished{SatoPollack10, author = {M.~Sato and R.~Pollack}, title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus}, note = {To appear in {\it Journal of Symbolic Computation}}}@article{GabbayPitts02, author = {M.~J.~Gabbay and A.~M.~Pitts}, title = {{A} {N}ew {A}pproach to {A}bstract {S}yntax with {V}ariable {B}inding}, journal = {Formal Aspects of Computing}, volume = {13}, year = 2002, pages = {341--363}}@article{Pitts03, author = {A.~M.~Pitts}, title = {{N}ominal {L}ogic, {A} {F}irst {O}rder {T}heory of {N}ames and {B}inding}, journal = {Information and Computation}, year = {2003}, volume = {183}, pages = {165--193}}@InProceedings{BengtsonParrow07, author = {J.~Bengtson and J.~Parrow}, title = {Formalising the pi-{C}alculus using {N}ominal {L}ogic}, booktitle = {Proc.~of the 10th International Conference on Foundations of Software Science and Computation Structures (FOSSACS)}, year = 2007, pages = {63--77}, series = {LNCS}, volume = {4423}}@inproceedings{BengtsonParow09, author = {J.~Bengtson and J.~Parrow}, title = {{P}si-{C}alculi in {I}sabelle}, booktitle = {Proc of the 22nd Conference on Theorem Proving in Higher Order Logics (TPHOLs)}, year = 2009, pages = {99--114}, series = {LNCS}, volume = {5674}}@inproceedings{TobinHochstadtFelleisen08, author = {S.~Tobin-Hochstadt and M.~Felleisen}, booktitle = {Proc.~of the 35rd Symposium on Principles of Programming Languages (POPL)}, title = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme}, publisher = {ACM}, year = {2008}, pages = {395--406}}@InProceedings{UrbanCheneyBerghofer08, author = "C.~Urban and J.~Cheney and S.~Berghofer", title = "{M}echanizing the {M}etatheory of {LF}", pages = "45--56", year = 2008, booktitle = "Proc.~of the 23rd IEEE Symposium on Logic in Computer Science (LICS)"}@InProceedings{UrbanZhu08, title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof", author = "C.~Urban and B.~Zhu", booktitle = "Proc.~of the 9th International Conference on Rewriting Techniques and Applications (RTA)", year = "2008", pages = "409--424", series = "LNCS", volume = 5117}@Article{UrbanPittsGabbay04, title = "{N}ominal {U}nification", author = "C.~Urban and A.M.~Pitts and M.J.~Gabbay", journal = "Theoretical Computer Science", pages = "473--497", volume = "323", number = "1-3", year = "2004"}@Article{Church40, author = {A.~Church}, title = {{A} {F}ormulation of the {S}imple {T}heory of {T}ypes}, journal = {Journal of Symbolic Logic}, year = {1940}, volume = {5}, number = {2}, pages = {56--68}}@Manual{PittsHOL4, title = {{S}yntax and {S}emantics}, author = {A.~M.~Pitts}, note = {Part of the documentation for the HOL4 system.}}@book{PaulsonBenzmueller, year={2009}, author={Benzm{\"u}ller, Christoph and Paulson, Lawrence C.}, title={Quantified Multimodal Logics in Simple Type Theory}, note={{http://arxiv.org/abs/0905.2435}}, series={{SEKI Report SR--2009--02 (ISSN 1437-4447)}}, publisher={{SEKI Publications}}}@Article{Cheney06, author = {J.~Cheney}, title = {{C}ompleteness and {H}erbrand {T}heorems for {N}ominal {L}ogic}, journal = {Journal of Symbolic Logic}, year = {2006}, volume = {71}, number = {1}, pages = {299--320}}