diff -r 4436039cc5e1 -r 05ccb61aa628 LMCS-Paper/document/root.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/LMCS-Paper/document/root.bib Fri Aug 12 22:37:41 2011 +0200 @@ -0,0 +1,319 @@ + +@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} +} +