pubs.bib

@ARTICLE{gacek12jar,
  author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
  title = {A Two-Level Logic Approach to Reasoning About Computations},
  journal = {Journal of Automated Reasoning},
  volume = 49,
  number = 2,
  year = 2012,
  month = AUG,
  pages = {241-273},
  ee = {http://dx.doi.org/10.1007/s10817-011-9218-1},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  pdf = {http://arxiv.org/pdf/0911.2993.pdf},
  arxiv = {http://arxiv.org/abs/0911.2993}
}

@INPROCEEDINGS{cofer12nfm,
  author = {Darren D. Cofer and Andrew Gacek and Steven P. Miller and
                  Michael W. Whalen and Brian LaValley and Lui Sha},
  title = {Compositional Verification of Architectural Models},
  booktitle = {NASA Formal Methods},
  year = 2012,
  pages = {126-140},
  ee = {http://dx.doi.org/10.1007/978-3-642-28891-3_13},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  pdf = {http://www.umsec.umn.edu/sites/all/files/NFM-springer-proof-72260126.pdf}
}

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

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

@ARTICLE{gacek11ic,
  author = {Andrew Gacek and Dale Miller and Gopalan Nadathur},
  title = {Nominal abstraction},
  journal = {Information and Computation},
  volume = 209,
  number = 1,
  year = 2011,
  pages = {48-73},
  ee = {http://dx.doi.org/10.1016/j.ic.2010.09.004},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  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://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}
}