pubs.bib

@ARTICLE{gacek12jar,
  author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
  title = {A two-level logic approach to reasoning about computations},
  year = 2012,
  journal = {Journal of Automated Reasoning},
  volume = 49,
  number = 2,
  pages = {241--273},
  pdf = {http://arxiv.org/pdf/0911.2993.pdf},
  arxiv = {http://arxiv.org/abs/0911.2993}
}

@PHDTHESIS{gacek09phd,
  title = {A Framework for Specifying, Prototyping, and
                  Reasoning about Computational Systems},
  author = {Andrew Gacek},
  school = {University of Minnesota},
  pdf = {https://arxiv.org/pdf/0910.0747.pdf},
  arxiv = {http://arxiv.org/abs/0910.0747},
  year = 2009,
  month = {September},
  slides = {http://abella-prover.org/slides/gacek09phd-slides.pdf}
}

@ARTICLE{gacek.na,
  author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
  title = {Nominal Abstraction},
  journal = {Information and Computation}
  volume = {209},
  number = 1,
  pages = {48--73},
  year = 2011,
  pdf = {http://arxiv.org/pdf/0908.1390.pdf},
  arxiv = {http://arxiv.org/abs/0908.1390}
}

@INPROCEEDINGS{gacek08lfmtp,
  author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
  title = {Reasoning in {A}bella about Structural Operational
                  Semantics Specifications},
  booktitle = {International Workshop on Logical Frameworks and
                  Meta-Languages: Theory and Practice (LFMTP 2008)},
  year = 2008,
  editor = {A. Abel and C. Urban},
  series = {Electronic Notes in Theoretical Computer Science},
  number = 228,
  pages = {85--100},
  pdf = {http://arxiv.org/pdf/0804.3914.pdf},
  slides = {http://abella-prover.org/slides/gacek08lfmtp-slides.pdf}
}

@INPROCEEDINGS{gacek08ijcar,
  author = {Andrew Gacek},
  title = {The {A}bella Interactive Theorem Prover (System
                  Description)},
  year = 2008,
  month = {August},
  booktitle = {Proceedings of IJCAR 2008},
  pages = {154--161},
  publisher = {Springer},
  series = {Lecture Notes in Artificial Intelligence},
  volume = 5195,
  editor = {A. Armando and P. Baumgartner and G. Dowek},
  pdf = {http://arxiv.org/pdf/0803.2305.pdf},
  slides = {http://abella-prover.org/slides/gacek08ijcar-slides.pdf}
}

@INPROCEEDINGS{wang13ppdp,
  author = {Yuting Wang and Kaustuv Chaudhuri and Andrew Gacek and Gopalan Nadathur}, 
  title = {Reasoning about higher-order relational specifications}
  booktitle = {Proceedings of PPDP 2013},
  note = {To appear},
  url = {http://arxiv.org/pdf/1302.2584.pdf}
}

@ARTICLE{mcdowell02tocl,
  author = {Raymond McDowell and Dale Miller},
  title = {Reasoning with Higher-Order Abstract Syntax in a
                  Logical Framework},
  journal = {ACM Transactions on Computational Logic},
  year = 2002,
  volume = 3,
  number = 1,
  pages = {80--136},
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/mcdowell01.pdf}
}

@ARTICLE{miller05tocl,
  author = {Dale Miller and Alwen Tiu},
  title = {A proof theory for generic judgments},
  journal = {ACM Transactions on Computational Logic},
  edited = {Phokion Kolaitis},
  month = {October},
  volume = 6,
  number = 4,
  pages = {749--783},
  publisher = {ACM Press},
  address = {New York, NY, USA},
  year = 2005,
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tocl-nabla.pdf}
}

@INPROCEEDINGS{nadathur88iclp,
  author = {Gopalan Nadathur and Dale Miller},
  title = {An {Overview} of {$\lambda$Prolog}},
  editors = {Kenneth A. Bowen and Robert A. Kowalski},
  booktitle = {{Fifth International Logic Programming Conference}},
  address = {Seattle},
  publisher = {MIT Press},
  pages = {810--827},
  month = {August},
  year = 1988,
  pdf = {http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/iclp88.pdf}
}