+ −
@Unpublished{KaliszykUrban11,+ −
author = {C.~Kaliszyk and C.~Urban},+ −
title = {{Q}uotients {R}evisited for {I}sabelle/{HOL}},+ −
note = {To appear in the Proc.~of the 26th ACM Symposium On Applied Computing},+ −
year = {2011}+ −
}+ −
+ −
@InProceedings{cheney05a,+ −
author = {J.~Cheney},+ −
title = {{S}crap your {N}ameplate ({F}unctional {P}earl)},+ −
booktitle = {Proc.~of the 10th ICFP Conference},+ −
pages = {180--191},+ −
year = {2005}+ −
}+ −
+ −
@Inproceedings{Altenkirch10,+ −
author = {T.~Altenkirch and N.~A.~Danielsson and A.~L\"oh and N.~Oury},+ −
title = {{PiSigma}: {D}ependent {T}ypes {W}ithout the {S}ugar},+ −
booktitle = "Proc.~of the 10th FLOPS Conference",+ −
year = 2010,+ −
series = "LNCS",+ −
pages = "40--55",+ −
volume = 6009+ −
}+ −
+ −
+ −
@InProceedings{ UrbanTasson05,+ −
author = "C. Urban and C. Tasson",+ −
title = "{N}ominal {T}echniques in {I}sabelle/{HOL}",+ −
booktitle = "Proc.~of the 20th CADE Conference",+ −
year = 2005,+ −
series = "LNCS",+ −
pages = "38--53",+ −
volume = 3632+ −
}+ −
+ −
@InProceedings{ UrbanBerghofer06,+ −
author = "C. Urban and S. Berghofer",+ −
title = "{A} {R}ecursion {C}ombinator for {N}ominal {D}atatypes {I}mplemented in {I}sabelle/{HOL}",+ −
booktitle = "Proc.~of the 3rd IJCAR Conference",+ −
year = 2006,+ −
series = "LNAI",+ −
volume = 4130,+ −
pages = "498--512"+ −
}+ −
+ −
@InProceedings{LeeCraryHarper07,+ −
author = {D.~K.~Lee and K.~Crary and R.~Harper},+ −
title = {{T}owards a {M}echanized {M}etatheory of {Standard ML}},+ −
booktitle = {Proc.~of the 34th POPL Symposium},+ −
year = 2007,+ −
pages = {173--184}+ −
}+ −
+ −
@Unpublished{chargueraud09,+ −
author = "A.~Chargu{\'e}raud",+ −
title = "{T}he {L}ocally {N}ameless {R}epresentation",+ −
Note = "To appear in J.~of Automated Reasoning." + −
}+ −
+ −
@article{NaraschewskiNipkow99,+ −
author={W.~Naraschewski and T.~Nipkow},+ −
title={{T}ype {I}nference {V}erified: {A}lgorithm {W} in {Isabelle/HOL}},+ −
journal={J.~of Automated Reasoning},+ −
year=1999,+ −
volume=23,+ −
pages={299--318}}+ −
+ −
@InProceedings{Berghofer99,+ −
author = {S.~Berghofer and M.~Wenzel},+ −
title = {{I}nductive {D}atatypes in {HOL} - {L}essons {L}earned in + −
{F}ormal-{L}ogic {E}ngineering},+ −
booktitle = {Proc.~of the 12th TPHOLs conference},+ −
pages = {19--36},+ −
year = 1999,+ −
volume = 1690,+ −
series = {LNCS}+ −
}+ −
+ −
@InProceedings{CoreHaskell,+ −
author = {M.~Sulzmann and M.~Chakravarty and S.~Peyton Jones and K.~Donnelly},+ −
title = {{S}ystem {F} with {T}ype {E}quality {C}oercions},+ −
booktitle = {Proc.~of the TLDI Workshop},+ −
pages = {53-66},+ −
year = {2007}+ −
}+ −
+ −
@inproceedings{cheney05,+ −
author = {J.~Cheney},+ −
title = {{T}oward a {G}eneral {T}heory of {N}ames: {B}inding and {S}cope},+ −
booktitle = {Proc.~of the 3rd MERLIN workshop},+ −
year = {2005},+ −
pages = {33-40}+ −
}+ −
+ −
@Unpublished{Pitts04,+ −
author = {A.~Pitts},+ −
title = {{N}otes on the {R}estriction {M}onad for {N}ominal {S}ets and {C}pos},+ −
note = {Unpublished 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}+ −
}+ −
+ −
@inproceedings{HuffmanUrban10,+ −
author = {B.~Huffman and C.~Urban},+ −
title = {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle},+ −
booktitle = {Proc.~of the 1st ITP Conference}, + −
pages = {35--50},+ −
volume = {6172},+ −
series = {LNCS},+ −
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 = {Unpublished notes.}+ −
}+ −
+ −
@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 = {J.~of Automated Reasoning},+ −
volume = 23,+ −
number = {1-4},+ −
year = 1999+ −
}+ −
+ −
@article{SatoPollack10,+ −
author = {M.~Sato and R.~Pollack},+ −
title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus},+ −
journal = {J.~of Symbolic Computation},+ −
volume = 45,+ −
pages = {598--616},+ −
year = 2010+ −
}+ −
+ −
@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 = {{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 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},+ −
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}+ −
}+ −
+ −