Current Work

I work on frameworks for specification, prototyping, and reasoning over computations. I am particularly interested in systems which manipulate objects with binding, e.g., programming languages and logics. I am the developer of the Abella system which allows for specification and interactive reasoning in this domain. This work is part of the SLIMMER Project and involves close collaboration with the Parsifal group at INRIA.

I graduated from the University of Minnesota with my PhD in September, 2009. I am now a post-doc for INRIA Saclay and I work with the Parsifal group in the Laboratoire d'Informatique (LIX) at École Polytechnique.

Publications

• A two-level logic approach to reasoning about computations, by Andrew Gacek, Dale Miller, and Gopalan Nadathur, Submitted 16 November, November 2009. [ bib | arXiv | .pdf ]
• A framework for specifying, prototyping, and reasoning about computational systems, by Andrew Gacek, Ph.D. thesis, University of Minnesota, September 2009. [ bib | arXiv | slides | .pdf ]
• Nominal abstraction, by Andrew Gacek, Dale Miller, and Gopalan Nadathur, Submitted 4 August, August 2009. [ bib | arXiv | .pdf ]
• The Abella interactive theorem prover (system description), by Andrew Gacek, Proceedings of IJCAR 2008 (A. Armando, P. Baumgartner, and G. Dowek, eds.), Lecture Notes in Artificial Intelligence, vol. 5195, Springer, August 2008, pp. 154-161. [ bib | slides | .pdf ]
• Combining generic judgments with recursive definitions, by Andrew Gacek, Dale Miller, and Gopalan Nadathur, Proceedings of LICS 2008 (F. Pfenning, ed.), IEEE Computer Society Press, June 2008, pp. 33-44. [ bib | slides | .pdf ]
• Reasoning in Abella about structural operational semantics specifications, by Andrew Gacek, Dale Miller, and Gopalan Nadathur, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008) (A. Abel and C. Urban, eds.), Electronic Notes in Theoretical Computer Science, no. 228, 2008, pp. 85-100. [ bib | slides | .pdf ]
• The Bedwyr system for model checking over syntactic expressions, by David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu, 21th Conference on Automated Deduction (Frank Pfenning, ed.), LNAI, no. 4603, Springer, 2007, pp. 391-397. [ bib | .pdf ]
• The suspension calculus and its relationship to other explicit treatments of substitution in lambda calculi, by Andrew Gacek, Master's thesis, University of Minnesota, December 2006. [ bib | slides | .pdf ]

Past Work

• September, 2009: Defended my PhD thesis: A Framework for Specifying, Prototyping, and Reasoning about Computational Systems.
• February, 2008: First public release of Abella, an interactive theorem prover based on lambda-tree syntax.
• December, 2007: Passed my oral preliminary exam and presented my doctoral thesis proposal.
• December, 2006: Defended my master's thesis: The Suspension Calculus and its Relationship to Other Explicit Treatments of Substitution in Lambda Calculi.
• June, 2005: Co-organized and presented at WIPS 2005: Workshop on Implementations of Proof Search.

Employment

• October, 2009 – current: Post-doc for INRIA Saclay in the Parsifal group.
• May, 2005 – September, 2009: Research assistant for Gopalan Nadathur.
• June – August, 2008: Intern at Rockwell Collins as part of the Automated Analysis group.
• August, 2006 – May, 2007: Consultant for Boston Scientific.
• June – July, 2006: Intern at École Polytechnique for the SLIMMER Project.
• January – May, 2005: Teaching assistant for CSci 3081: Program Design and Development.
• May – August, 2004: Intern at United Defense. Web application development and deployment for document management system.
• May – August, 2003: Intern at United Defense. Data migration and cleansing for document management system.
• 2002 – 2003: Research Assistant for Victor Winter at the University of Nebraska at Omaha. Implemented rewriting based "Mini-Java" complier and class loader for Sandia Secure Processor Project.
• July – August, 2000: Junior Counselor for PROMYS Program, an intensive summer school on number theory.

Education

• Ph.D. Computer Science, University of Minnesota, 2009
• M.S. Computer Science, University of Minnesota, 2006
• B.S. Computer Science and Mathematics, University of Nebraska at Omaha, 2004.

Awards

• 2008: Second place in the CADE Squash Competition.
• 2006: State squash champion in the 2.5 (and below!) division

  (There was only one other person in that division)

• 2004: Academic Excellence Fellowship from the University of Minnesota's Computer Science department.
• 2004: Dean's Award for Computer Science and Vice Chancellor's Award at University of Nebraska at Omaha.
• 2002: Placed 61st in the nation on the William Lowell Putnam Mathematical Competition.
• 2000 – 2004: Eight semester winner of the UNO Problem of the Week.
• 2000 – 2004: Walter Scott, Jr. Scholarship from the Peter Kiewit Institute.