Current Work

I am a fifth year Ph.D. student studying logic and programming languages under the direction of my advisor, Gopalan Nadathur. My focus on is frameworks for specification and reasoning, particularly over 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 am also involved with the programming languages seminar here at the U of M. I have presented topics such as the POPLmark challenge, the Twelf system, Kruskal's theorem, and recursive path orderings. Possible topics for future presentations are the ACL2 and Coq theorem proving systems.

Publications

• 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 | .pdf ]

Past Work

• 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: Finished my master's thesis on the suspension calculus.
• June, 2005: Co-organized and presented at WIPS 2005: Workshop on Implementations of Proof Search.

Employment

• May, 2005 – Current: 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

• 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.