@article{appel+03,
  author =       {A. Appel and N. Michael and A. Stump and R. Virga},
  title =        {{A Trustworthy Proof Checker}},
  journal =    {Journal of Automated Reasoning, special issue on Proof-Carrying Code},
  volume = "31",
  number = "3-4",
  pages="231--260",
  year =         "2003"
}

@inproceedings{stump03,
author= "A. Stump",
title={{Subset Types and Partial Functions}},
booktitle="19th International Conference on Automated Deduction",
pages="151-165",
editor="F. Baader",
year="2003"}

@inproceedings{stump+03,
author="A. Stump and A. Deivanayagam and S. Kathol and D. Lingelbach and D. Schobel",
title={{Rogue Decision Procedures}},
booktitle="1st International Workshop on Pragmatics of Decision Procedures in Automated Reasoning",
editor="C. Tinelli and S. Ranise",
year=2003}

@inproceedings{wu+03,
title={{Foundational Proof Checkers with Small Witnesses}},
author="D. Wu and A. Appel and A. Stump",
booktitle="5th ACM-SIGPLAN International Conference on
Principles and Practice of Declarative Programming",
editor="D. Miller",
pages={264--274},
year=2003}

@inproceedings{stump+04a,
author="A. Stump and R. Besand and J. Brodman and J. Hseu and B. Kinnersley",
title={{From Rogue to MicroRogue}},
booktitle="International Workshop on Rewriting Logic and Applications",
editor="N. Marti-Oliet",
year=2004}

@inproceedings{stump04b,
author="A. Stump",
title={{Imperative LF Meta-Programming}},
booktitle="4th International Workshop on Logical Frameworks and Meta-Languages",
editor={{C. Sch\"{u}rmann}},
year=2004}

@inproceedings{stump+04c,
author="A. Stump and C. Sch{\"{u}}rmann",
title={{Logical Semantics for the Rewriting Calculus}},
booktitle="5th International Workshop on Strategies in Automated Deduction",
editor={{M. Bonacina and T. Boy de la Tour}},
year=2004}

@inproceedings{klapper+04,
author="R. Klapper and A. Stump",
title={{Validated Proof-Producing Decision Procedures}},
booktitle="2nd International Workshop on Pragmatics of Decision Procedures in Automated Reasoning",
editor="C. Tinelli and S. Ranise",
year=2004}

@inproceedings{stump+05,
author="A. Stump and L.-Y. Tan",
title={{The Algebra of Equality Proofs}},
booktitle="16th International Conference on Rewriting Techniques and Applications",
editor="J{\"{u}}rgen Giesl",
pages="469--483",
publisher="Springer",
year=2005}

@mastersthesis{brandt+05,
 author="Joel Brandt",
 title={{What a Mesh: Dependent Data Types for Correct Mesh Manipulation Algorithms}},
 school={{Washington University in Saint Louis}},
 year="2005",
 month="April",
note="Available from \url{http://cl.cse.wustl.edu}"
}

@inproceedings{wehrman+05,
author = "Ian Wehrman and Aaron Stump",
editor = "A. Armando and A. Cimatti",
title={{Mining Propositional Simplification Proofs for Small Validating Clauses}},
booktitle="3rd International Workshop on Pragmatics of Decision Procedures in Automated Reasoning",
year=2005}

@inproceedings{stump05a,
author="A. Stump",
editor="W. Ahrendt and P. Baumgartner and H. de Nivelle",
booktitle="CADE Workshop on Disproving",
title="Validated Construction of Congruence Closures",
year=2005}

@inproceedings{stump05b,
author="A. Stump",
booktitle="Verified Software: Theories, Tools, Experiments",
editor="N. Shankar",
title="Programming with Proofs: Language-Based Approaches to Totally Correct Software",
year=2005}

@inproceedings{westbrook+05a,
author="E. Westbrook and A. Stump and I. Wehrman",
title={{A Language-based Approach to Functionally Correct Imperative Programming}},
booktitle="Proceedings of the 10th International Conference on Functional Programming (ICFP05)",
location="Tallinn, Estonia",
year="2005"}

@techreport{westbrook+05b,
author="E. Westbrook and A. Stump and I. Wehrman",
title={{A Language-based Approach to Functionally Correct Imperative Programming}},
institution = {{Washington University in Saint Louis}},
number = "WUCSE-2005-32",
month = "July",
year = "2005"}

@inproceedings{barrett+05a,
      author= "C. Barrett and L. de Moura and A. Stump",
      title={{SMT-COMP: Satisfiability Modulo Theories Competition}},
      booktitle="17th International Conference on Computer Aided Verification",
      editor="K. Etessami and S. Rajamani",
      pages={20--23},
      publisher="Springer",
      year="2005"}

@article{barrett+05b,
      author= "C. Barrett and L. de Moura and A. Stump",
      title={{Design and Results of the 1st Satisfiability Modulo Theories Competition (SMT-COMP 2005)}},
      journal="Journal of Automated Reasoning",
      pages={373--390},
      publisher="Springer",
      volume=35,
      number=4,
      year=2005}

@article{stump+06,
title={{Knuth-Bendix Completion of Theories of Commuting Group Endomorphisms}},
author="A. Stump and B. L{\"o}chner",
journal="Information Processing Letters",
year=2006,
volume=98,
pages="195--198"}

@inproceedings{stump+06,
author="A. Stump and I. Wehrman",
title={{Property Types: Semantic Programming for Java}},
booktitle="International Conference on Foundations of Object-Oriented Languages (FOOL/WOOD)",
year=2006,
editor="C. Stone",
note="affiliated with POPL 2006"}.

@inproceedings{wehrman+06,
  author="I. Wehrman and A. Stump and E. Westbrook",
  title={{Slothrop: Knuth-Bendix Completion with Modern Termination Checking}},
  booktitle = {17th International Conference on Term Rewriting and Applications},
  pages     = {287-296},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4098},
  location = "Seattle, WA",
  year      = {2006},
  editor    = {F. Pfenning}
}

@inproceedings{westbrook06a,
author="E. Westbrook",
title="Free Variable Types",
booktitle="Seventh Symposium on Trends in Functional Programming (TFP 06)",
year="2006",
month="April"
}

@inproceedings{westbrook06b,
author="Edwin Westbrook",
title="Pattern Solutions to Higher-Order Unification Problems",
booktitle="20th International Workshop on Unification (UNIF 06)",
year="2006",
month="August"
}

@techreport{tan06,
author="Li-Yang Tan",
title={{The Meta-Theory of $Q_0$ in the Calculus of Inductive Constructions}},
institution = {{Washington University in Saint Louis}},
number = "WUCSE-2006-24",
month = "May",
year = "2006"}

@mastersthesis{delaware07,
 author="B. Delaware",
 title={{Baghak: Developing Sound and Complete Decision Procedures in
Coq}},
 school={{Washington University in Saint Louis}},
 year="2007",
 month="August",
note="Available from \url{http://clc.cs.uiowa.edu}"
}

@inproceedings{zeller+07,
author="M. Zeller and A. Stump and M. Deters",
title={{Signature Compilation for the Edinburgh Logical Framework}},
booktitle="Workshop on Logical Frameworks and Meta-Languages: Theory
and Practice (LFMTP)",
year = 2007,
editor="C. Sch{\"u}rmann"}

@article{barrett+06,
 author = {C. Barrett and L. de Moura and A. Stump},
 title = {{Design and Results of the 2nd Annual Satisfiability Modulo Theories competition (SMT-COMP 2006)}},
 journal = {Formal Methods in System Design},
 volume = {31},
 number = {3},
 year = {2007},
 pages = {221--239}
 }

@article{barrett+07,
 author = {C. Barrett and M. Deters and A. Oliveras and A. Stump},
 title = {{Design and Results of the 3rd Annual Satisfiability Modulo Theories competition (SMT-COMP 2007)}},
 journal = {International Journal of Artificial Intelligence Tools},
volume=17,
number=4,
pages={569--606},
year=2008
 }

@article{stump09,
author="A. Stump",
title ={{Directly Reflective Meta-Programming}},
journal={Higher-Order and Symbolic Computation},
volume=22,
number=2,
pages="115--144",
year=2009}

@inproceedings{stump+08a,
author="A. Stump and D. Oe",
title={{Towards an SMT Proof Format}},
booktitle="International Workshop on Satisfiability Modulo Theories",
editor="C. Barrett and L. de Moura",
year=2008}


@inproceedings{stump08b,
author="A. Stump",
title={{Proof Checking Technology for Satisfiability Modulo Theories}},
booktitle="Logical Frameworks and Meta-Languages: Theory and Practice",
editor="A. Abel and C. Urban",
year=2008}

@mastersthesis{petcher08,
 author="A. Petcher",
 title={{Deciding Joinability Modulo Ground Equations in                              
Operational Type Theory.}},
 school={{Washington University in Saint Louis}},
 year="2008",
 month="May",
note="Available from \url{http://www.cs.uiowa.edu/~astump}"
}

@inproceedings{petcher+09,
author="A. Petcher and A. Stump",
title = {{Deciding Joinability Modulo Ground Equations in Operational Type Theory}},
booktitle="Proof Search in Type Theories (PSTT), workshop affiliated with the Conference on Automated Deduction (CADE)",
year=2009,
editor="S. Lengrand and D. Miller"}

@inproceedings{oe+09,
author="D. Oe and A. Reynolds and A. Stump",
title={{Fast and Flexible Proof Checking for SMT}},
booktitle="Workshop on Satisfiability Modulo Theories (SMT)",
year=2009,
editor="B. Dutertre and O. Strichman"}

@inproceedings{stump+09,
title={{Verified Programming in Guru}},
author="A. Stump and M. Deters and A. Petcher and T. Schiller and T. Simpson",
booktitle="Programming Languges meets Program Verification (PLPV)",
editor="T. Altenkirch and T. Millstein",
year=2009}

@inproceedings{stump+10,
  author    = {A. Stump and
               E. Austin},
  title     = {{Resource Typing in Guru}},
  booktitle = {Proceedings of the 4th ACM Workshop Programming Languages
               meets Program Verification, PLPV 2010, Madrid, Spain, January
               19, 2010},
  year      = {2010},
  pages     = {27-38},
  editor    = {J.-C. Filli{\^a}tre and
               C. Flanagan},
  publisher = {ACM},
  year      = {2010},
}

@inproceedings{stump+10b,
  author    = {A. Stump and
               V. Sj{\"o}berg and
               S. Weirich},
  title     = {{Termination Casts: A Flexible Approach to Termination with
               General Recursion}},
  booktitle = {Proceedings Workshop on Partiality and Recursion in Interactive
               Theorem Provers},
  year      = {2010},
  pages     = {76-93},
  editor    = {A. Bove and
               E. Komendantskaya and
               M. Niqui},
  series    = {EPTCS},
  volume    = {43},
  year      = {2010},
}