
@article{AMSV03,
  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{S03,
author= "A. Stump",
title={{Subset Types and Partial Functions}},
booktitle="19th International Conference on Automated Deduction",
pages="151-165",
editor="F. Baader",
year="2003"}

@article{S03a,
author= "A. Stump",
title={{Subset Types and Partial Functions}},
journal={draft paper available from author's homepage},
year="2003"}

@inproceedings{s03b,
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{was03,
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{s04j,
author="A. Stump and R. Dickinson and J. Brodman",
title={{Automata Manipulation in Rogue}},
booktitle="Compiler Construction",
note="Under review.",
editor="E. Duesterwald",
year=2004}

@inproceedings{s04,
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{s04rsp_foo,
author="A. Stump",
title={{Static Validation of Proof-Producing Decision Procedures}},
editor="D. Basin and M. Rusinowitch",
booktitle="International Joint Conference on Automated Reasoning",
year=2004,
note="under review"}

@inproceedings{s04rsp,
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{stumpschurmann04,
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{klapperstump04,
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}

@article{westbrookstump04,
author="E. Westbrook and A. Stump",
title={{Exclusive Resource Access with Temporal Types}},
journal="in preparation",
year=2004}

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

@inproceedings{ksww05,
author="R. Klapper and A. Stump and I. Wehrman and E. Westbrook",
title={{Validated Algebraic Proof-Mining for EUF}},
booktitle="20th International Conference on Automated Deduction",
editor="R. Niewenhuis",
note="under review",
year=2005}

@mastersthesis{Joel05,
 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{wehrmanstump05,
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{stump-disproving05,
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{stump-vstte05,
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}

%was westbrostump05,
@inproceedings{wsw-icfp05,
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{wsw05-tech,
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+05,
      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}

% also SL06
@article{stumploechner06,
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{stumpwehrman06,
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{stump06a,
author="A. Stump",
title={{POPLmark 1a with Named Bound Variables}},
booktitle={{Informal Workshop on the POPLmark Challenge}},
editor="B. Pierce",
year="2006"}

% also wehrmanstump06
@inproceedings{wsw-rta06,
  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}
}

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

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

@techreport{tan-ms-thesis,
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"}

@article{stump06,
title={{Local Scope-Safe Meta-Programming in Untyped Lambda Calculus}},
journal={{Higher Order and Symbolic Computation}},
author="A Stump",
note="Currently under review.",
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://cl.cse.wustl.edu}"
}

@inproceedings{zeller07,
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{stump08,
author="A. Stump",
title ={{Directly Reflective Meta-Programming}},
journal={Higher-Order and Symbolic Computation},
note="to appear",
year=2008}

@inproceedings{SO08,
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}"
}

@manuscript{optt,
author="A. Stump and E. Westbrook",
title={{A Core Operational Type Theory}},
note="Under review, available from \url{http://www.cs.uiowa.edu/~astump}"}
year=2008}

@manuscript{guru08,
title={{Verified Programming in Guru}},
author="A. Stump and M. Deters and A. Petcher and T. Schiller and T. Simpson",
note="Under review, available from \url{http://www.cs.uiowa.edu/~astump}",
year=2008}