+ −
@Unpublished{Pitts04,+ −
author = {Andrew Pitts},+ −
title = {{N}otes on the {R}estriction {M}onad for {N}ominal {S}ets and {C}pos},+ −
note = {Notes for an invited talk given at CTCS},+ −
year = {2004}+ −
}+ −
+ −
@incollection{UrbanNipkow09,+ −
author = {C.~Urban and T.~Nipkow},+ −
title = {{N}ominal {V}erification of {A}lgorithm {W}},+ −
booktitle={From Semantics to Computer Science. Essays in Honour of Gilles Kahn},+ −
editor={G.~Huet and J.-J.~L{\'e}vy and G.~Plotkin},+ −
publisher={Cambridge University Press},+ −
pages={363--382},+ −
year=2009+ −
}+ −
+ −
@InProceedings{Homeier05,+ −
author = {P.~Homeier},+ −
title = {{A} {D}esign {S}tructure for {H}igher {O}rder {Q}uotients},+ −
booktitle = {Proc.~of the 18th TPHOLs Conference},+ −
pages = {130--146},+ −
year = {2005},+ −
volume = {3603},+ −
series = {LNCS}+ −
}+ −
+ −
@article{ott-jfp,+ −
author = {P.~Sewell and + −
F.~Z.~Nardelli and + −
S.~Owens and + −
G.~Peskine and + −
T.~Ridge and + −
S.~Sarkar and + −
R.~Strni\v{s}a},+ −
title = {{Ott}: {E}ffective {T}ool {S}upport for the {W}orking {S}emanticist},+ −
journal = {J.~of Functional Programming},+ −
year = {2010},+ −
volume = {20},+ −
number = {1},+ −
pages = {70--122}+ −
}+ −
+ −
@INPROCEEDINGS{Pottier06,+ −
author = {F.~Pottier},+ −
title = {{A}n {O}verview of {C$\alpha$ml}},+ −
year = {2006},+ −
booktitle = {ACM Workshop on ML},+ −
pages = {27--52},+ −
volume = {148},+ −
number = {2},+ −
series = {ENTCS}+ −
}+ −
+ −
@Unpublished{HuffmanUrban10,+ −
author = {B.~Huffman and C.~Urban},+ −
title = {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle},+ −
note = {To appear at {\it ITP'10 Conference}},+ −
annote = {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf},+ −
year = {2010}+ −
}+ −
+ −
@PhdThesis{Leroy92,+ −
author = {X.~Leroy},+ −
title = {{P}olymorphic {T}yping of an {A}lgorithmic {L}anguage},+ −
school = {University Paris 7},+ −
year = {1992},+ −
note = {INRIA Research Report, No~1778}+ −
}+ −
+ −
@Unpublished{SewellBestiary,+ −
author = {P.~Sewell},+ −
title = {{A} {B}inding {B}estiary},+ −
note = {Personal communication.}+ −
}+ −
+ −
@InProceedings{challenge05,+ −
author = {B.~E.~Aydemir and A.~Bohannon and M.~Fairbairn and+ −
J.~N.~Foster and B.~C.~Pierce and P.~Sewell and + −
D.~Vytiniotis and G.~Washburn and S.~Weirich and+ −
S.~Zdancewic},+ −
title = {{M}echanized {M}etatheory for the {M}asses: {T}he \mbox{Popl}{M}ark + −
{C}hallenge},+ −
booktitle = {Proc.~of the 18th TPHOLs Conference},+ −
pages = {50--65},+ −
year = {2005},+ −
volume = {3603},+ −
series = {LNCS}+ −
}+ −
+ −
@article{MckinnaPollack99,+ −
author = {J.~McKinna and R.~Pollack},+ −
title = {{S}ome {T}ype {T}heory and {L}ambda {C}alculus {F}ormalised},+ −
journal = {Journal of Automated Reasoning},+ −
volume = 23,+ −
number = {1-4},+ −
year = 1999+ −
}+ −
+ −
@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 J.~of Symbolic Computation}}+ −
}+ −
+ −
@article{GabbayPitts02,+ −
author = {M.~J.~Gabbay and A.~M.~Pitts},+ −
title = {A New Approach to Abstract Syntax with Variable+ −
Binding},+ −
journal = {Formal Aspects of Computing},+ −
volume = {13},+ −
year = 2002,+ −
pages = {341--363}+ −
}+ −
+ −
@article{Pitts03,+ −
author = {A.~M.~Pitts},+ −
title = {Nominal Logic, A First Order Theory of Names and+ −
Binding},+ −
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 FOSSACS Conference},+ −
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 TPHOLs Conference},+ −
year = 2009,+ −
pages = {99--114},+ −
series = {LNCS},+ −
volume = {5674}+ −
}+ −
+ −
@inproceedings{TobinHochstadtFelleisen08,+ −
author = {S.~Tobin-Hochstadt and M.~Felleisen},+ −
booktitle = {Proc.~of the 35rd POPL Symposium},+ −
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 LICS Symposium"+ −
}+ −
+ −
@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 RTA Conference",+ −
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 theorems for {N}ominal {L}ogic},+ −
journal = {Journal of Symbolic Logic},+ −
year = {2006},+ −
volume = {71},+ −
number = {1},+ −
pages = {299--320}+ −
}+ −
+ −