pubs.bib

@INPROCEEDINGS{gacek10ppdp,
  author = {Andrew Gacek},
  title = {Relating Nominal and Higher-order Abstract Syntax
                  Specifications},
  booktitle = {PPDP '10: Proceedings of the 2010 Symposium on Principles and
                  Practice of Declarative Programming},
  year = 2010,
  publisher = {ACM},
  month = {July},
  pages = {177--186},
  pdf = {http://arxiv.org/pdf/1003.5447.pdf},
  slides = {http://www.cs.umn.edu/~agacek/pubs/slides/gacek10ppdp-slides.pdf}
}

@UNPUBLISHED{gacek.twolevel,
  author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
  title = {A two-level logic approach to reasoning about computations},
  year = 2009,
  month = {November},
  pdf = {http://arxiv.org/pdf/0911.2993.pdf},
  arxiv = {http://arxiv.org/abs/0911.2993},
  note = {Submitted}
}

@PHDTHESIS{gacek09phd,
  title = {A Framework for Specifying, Prototyping, and Reasoning about
                  Computational Systems},
  author = {Andrew Gacek},
  school = {University of Minnesota},
  pdf = {http://www.cs.umn.edu/~agacek/pubs/gacek-thesis/gacek-thesis.pdf},
  arxiv = {http://arxiv.org/abs/0910.0747},
  year = 2009,
  month = {September},
  slides = {http://www.cs.umn.edu/~agacek/pubs/slides/gacek09phd-slides.pdf}
}

@UNPUBLISHED{gacek.na,
  author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
  title = {Nominal Abstraction},
  year = 2009,
  month = {August},
  pdf = {http://arxiv.org/pdf/0908.1390.pdf},
  arxiv = {http://arxiv.org/abs/0908.1390},
  note = {Submitted}
}

@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://www.cs.umn.edu/~agacek/pubs/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://www.cs.umn.edu/~agacek/pubs/slides/gacek08ijcar-slides.pdf}
}

@INPROCEEDINGS{gacek08lics,
  author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
  title = {Combining generic judgments with recursive definitions},
  booktitle = {Proceedings of LICS 2008},
  month = {June},
  year = 2008,
  pages = {33--44},
  editor = {F. Pfenning},
  publisher = {IEEE Computer Society Press},
  url = {http://arxiv.org/pdf/0802.0865.pdf},
  slides = {http://www.cs.umn.edu/~agacek/pubs/slides/gacek08lics-slides.pdf}
}

@INPROCEEDINGS{baelde07cade,
  title = {The {Bedwyr} system for model checking over syntactic
                  expressions},
  author = {David Baelde and Andrew Gacek and Dale Miller and Gopalan
                  Nadathur and Alwen Tiu},
  booktitle = {21th Conference on Automated Deduction},
  pages = {391--397},
  year = 2007,
  editor = {Frank Pfenning},
  number = 4603,
  series = {LNAI},
  publisher = {Springer},
  pdf = {http://arxiv.org/pdf/cs/0702116.pdf}
}

@MASTERSTHESIS{gacek06msthesis,
  author = {Andrew Gacek},
  title = {The Suspension Calculus and its Relationship to Other
                  Explicit Treatments of Substitution in Lambda Calculi},
  school = {University of Minnesota},
  year = 2006,
  month = {December},
  pdf = {http://arxiv.org/pdf/cs/0702027.pdf},
  slides = {http://www.cs.umn.edu/~agacek/pubs/slides/gacek06msthesis-slides.pdf}
}