pubs.bib

@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 16 November}
}

@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 4 August}
}

@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}
}