Current Work

I am a fourth 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 a 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

• Reasoning in Abella about structural operational semantics specifications, by Andrew Gacek, Dale Miller, and Gopalan Nadathur, Available from http://arxiv.org/abs/0804.3914. Draft submitted April 23, 2008. [ bib | .pdf ]
• System description: Abella - A system for reasoning about computations, by Andrew Gacek, 2008, Available from http://arxiv.org/abs/0803.2305. To appear in IJCAR. [ bib | .pdf ]
• Combining generic judgments with recursive definitions, by Andrew Gacek, Dale Miller, and Gopalan Nadathur, 23th Symposium on Logic in Computer Science (F. Pfenning, ed.), IEEE Computer Society Press, 2008, To appear. [ bib | .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 subsubstitution 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.
• 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

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