--- a/Pearl-jv/document/root.bib Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,171 +0,0 @@
-@Article{ Urban08,
- author = "C. Urban",
- title = "{N}ominal {T}echniques in {I}sabelle/{HOL}",
- journal = "Journal of Automated Reasoning",
- volume = "40",
- number = "4",
- pages = "327--356",
- year = "2008"
-}
-
-@InProceedings{norrish04,
- author = {M.~Norrish},
- title = {{R}ecursive {F}unction {D}efinition for {T}ypes with {B}inders},
- booktitle = {Proc.~of the 17th International Conference Theorem Proving in
- Higher Order Logics (TPHOLs)},
- pages = {241--256},
- year = {2004},
- volume = {3223},
- series = {LNCS}
-}
-
-@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}
-}
-
-@InProceedings{AydemirBohannonWeirich07,
- author = {B.~Aydemir and A.~Bohannon and S.~Weihrich},
- title = {{N}ominal {R}easoning {T}echniques in {C}oq ({E}xtended {A}bstract)},
- booktitle = {Proc.~of the 2st International Workshop on Logical Frameworks and Meta-Languages:
- Theory and Practice (LFMTP)},
- pages = {69--77},
- year = {2007},
- 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}
-}
-
-@Manual{Wenzel04,
- title = {{U}sing {A}xiomatic {T}ype {C}lasses in {I}sabelle},
- author = {M.~Wenzel},
- note = {Manual in the Isabelle distribution.}
-}
\ No newline at end of file