| 2014 | ICFP | Romeo: a system for more flexible binding-safe programming. | Paul Stansifer, Mitchell Wand |
| 2011 | POPL | A separation logic for refining concurrent objects. | Aaron Joseph Turon, Mitchell Wand |
| 2009 | VMCAI | The Higher-Order Aggregate Update Problem. | Christos Dimoulas, Mitchell Wand |
| 2008 | Coordination | A Compositional Trace Semantics for Orc. | Dimitrios Vardoulakis, Mitchell Wand |
| 2008 | ESOP | A Theory of Hygienic Macros. | David Herman, Mitchell Wand |
| 2006 | ESOP | Bisimulations for Untyped Imperative Objects. | Vasileios Koutavas, Mitchell Wand |
| 2006 | POPL | Small bisimulations for reasoning about higher-order imperative programs. | Vasileios Koutavas, Mitchell Wand |
| 2005 | ESOP | Bottom-Up beta-Reduction: Uplinks and lambda-DAGs. | Olin Shivers, Mitchell Wand |
| 2004 | ICFP | Relating models of backtracking. | Mitchell Wand, Dale Vaillancourt |
| 2003 | ICFP | Understanding aspects: extended abstract. | Mitchell Wand |
| 2002 | ESOP | A Modular, Extensible Proof Method for Small-Step Flow Analyses. | Mitchell Wand, Galen B. Williamson |
| 1999 | ICFP | Trampolined Style. | Steven E. Ganz, Daniel P. Friedman, Mitchell Wand |
| 1999 | OOPSLA | A Language for Specifying Recursive Traversals of Object Structures. | Johan Ovlinger, Mitchell Wand |
| 1999 | POPL | Constraint Systems for Useless Variable Elimination. | Mitchell Wand, Igor Siveroni |
| 1997 | POPL | Denotational Semantics Using an Operationally-Based Term Model. | Mitchell Wand, Gregory T. Sullivan |
| 1996 | Coordination | Compiler Correctness for Concurrent Languages. | David S. Gladstein, Mitchell Wand |
| 1996 | ECOOP | Modeling Subobject-based Inheritance. | Jonathan G. Rossie Jr., Daniel P. Friedman, Mitchell Wand |
| 1994 | POPL | Selective and Lightweight Closure Conversion. | Mitchell Wand, Paul Steckler |
| 1994 | SAS | Selective Thunkification. | Paul Steckler, Mitchell Wand |
| 1993 | POPL | Specifying the Correctness of Binding-Time Analysis. | Mitchell Wand |
| 1992 | ESOP | Type Inference for Partial Types is Decidable. | Patrick O'Keefe, Mitchell Wand |
| 1991 | MFPS | Correctness of Procedure Representations in Higher-Order Assembly Language. | Mitchell Wand |
| 1990 | LICS | Conditional Lambda-Theories and the Verification of Static Properties of Programs | Mitchell Wand, Zheng-Yu Wang |
| 1989 | LICS | Type Inference for Record Concatenation and Multiple Inheritance | Mitchell Wand |
| 1988 | LICS | Corrigendum: Complete Type Inference for Simple Objects | Mitchell Wand |
| 1988 | POPL | Correct Flow Analysis in Continuation Semantics. | Margaret Montenyohl, Mitchell Wand |
| 1987 | LICS | Complete Type Inference for Simple Objects | Mitchell Wand |
| 1987 | POPL | Macro-by-Example: Deriving Syntactic Transformations from their Specifications. | Eugene E. Kohlbecker, Mitchell Wand |
| 1986 | POPL | Finding the Source of Type Errors. | Mitchell Wand |
| 1985 | POPL | Embedding Type Structure in Semantics. | Mitchell Wand |
| 1984 | POPL | A Types-as-Sets Semantics for Milner-Style Polymorphism. | Mitchell Wand |
| 1983 | POPL | Loops in Combinator-Based Compilers. | Mitchell Wand |
| 1982 | POPL | Semantics-Directed Machine Architecture. | Mitchell Wand |
| 1976 | ISSAC | Recursive programming through table look-up. | Daniel P. Friedman, David S. Wise, Mitchell Wand |
| 1976 | STOC | A New Incompleteness Result for Hoare's System | Mitchell Wand |
| 1973 | STOC | An Unusual Application of Program-Proving | Mitchell Wand |
| 1972 | ICALP | A Concrete Approach to Abstract Recursion Definitions. | Mitchell Wand |