@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}+ −
}+ −
+ −