@UNPUBLISHED{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}, 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, 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{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} }