Books
Editor of Conference Proceedings
-
Static analysis,
Springer-Verlag (LNCS 1824), 2000.
Proceedings of SAS'00, 7th International Static Analysis Symposium.
-
Proceedings of PASTE'02,
Program Analysis for Software Tools and Engineering,
with Matthew B. Dwyer.
ACM SIGPLAN-SIGSOFT Workshop, ACM Press, 2002.
-
Proceedings of POPL'05,
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
ACM Press, 2005.
General chair: Jens Palsberg.
Program chair: Martin Abadi.
-
Proceedings of TACAS'06,
International Conference on Tools and Algorithms for the
Construction and Analysis of Systems,
with Holger Hermanns.
Springer-Verlag, 2006.
-
Proceedings of MEMOCODE'06,
ACM-IEEE Conference on Formal Methods and Programming Models for Co-Design,
with James Hoe.
IEEE Press, 2006.
-
Proceedings of SPIN'08,
Model Checking Software, 15th International SPIN Workshop,
with Klaus Havelund and Rupak Majumdar.
Springer-Verlag, 2008.
-
Proceedings of EMSOFT'08,
International Conference on Embedded Software,
with Luca de Alfaro.
ACM Press, 2008.
-
Proceedings of SAS'09,
International Static Analysis Symposium,
with Zhendong Su.
Springer (LNCS 5673), 2009.
-
Semantics and Algebraic Specification,
Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday.
Springer (LNCS 5700), 2009.
-
Proceedings of POPL'10,
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
ACM Press, 2010.
General chair: Manuel Hermenegildo.
Program chair: Jens Palsberg.
-
Proceedings of X10,
ACM SIGPLAN X10 Workshop: 2012 (Beijing).
-
Proceedings of VMCAI'18,
International Conference on
Verification, Model Checking, and Abstract Interpretation,
with Isil Dillig.
2018 (Los Angeles).
Journal Articles
-
Safety analysis versus type inference for
partial types,
with Michael I. Schwartzbach.
Information Processing Letters, 43:175-180, 1992.
-
Normal forms have partial types.
Information Processing Letters, 45:1-3, 1993.
-
Correctness of binding-time analysis.
Journal of Functional Programming, 3(3):347-363, 1993.
-
A denotational semantics of inheritance and its correctness, with William
Cook.
Information and Computation, 114(2):329-350, 1994.
Preliminary version in Proceedings of OOPSLA'89, ACM SIGPLAN Fourth Annual
Conference on Object-Oriented Programming Systems, Languages and
Applications, pages 433-443, New Orleans, Louisiana, October 1989.
-
Static typing for object-oriented programming, with Michael I.
Schwartzbach.
Science of Computer Programming, 23(1):19-53, 1994.
-
Efficient inference of partial types, with Dexter Kozen and Michael I.
Schwartzbach.
Journal of Computer and System Sciences, 49(2):306-324, 1994.
Preliminary version in Proceedings of FOCS'92, 33rd IEEE Symposium on
Foundations of Computer Science, pages 363-371, Pittsburgh, Pennsylvania,
October 1992.
-
Safety analysis versus type inference, with Michael I. Schwartzbach.
Information and Computation, 118(1):128-141, 1995.
-
Efficient recursive subtyping, with Dexter Kozen and Michael I.
Schwartzbach.
Mathematical Structures in Computer Science, 5(1):113-125,
1995.
Preliminary version in Proceedings of POPL'93, Twentieth Annual
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages
419-428, Charleston, South Carolina, January 1993.
-
Complexity results for 1-safe nets, with Allan Cheng and Javier Esparza.
Theoretical Computer Science, 147(1-2):117-136, 1995.
Preliminary version in Proceedings of FST&TCS 13, Thirteenth Conference on
the Foundations of Software Technology & Theoretical Computer Science,
Springer-Verlag (LNCS 761), pages 326-337, Bombay, India, December
1993.
-
The essence of eta-expansion in partial evaluation, with Olivier Danvy and
Karoline Malmkjaer.
Lisp and Symbolic Computation, 8(3):209-227, 1995.
Preliminary version in Proceedings of PEPM'94, ACM SIGPLAN Workshop on Partial
Evaluation and Semantics-Based Program Manipulation, pages 11-20, Orlando,
Florida, June 1994.
-
Closure analysis in constraint form.
ACM Transactions on Programming Languages and Systems,
17(1):47-62, January 1995.
Preliminary version in Proceedings of CAAP'94, Colloquium on Trees in Algebra
and Programming, Springer-Verlag (LNCS 787), pages 276-290,
Edinburgh, Scotland, April 1994.
-
Efficient implementation of adaptive software, with Cun Xiao and Karl
Lieberherr.
ACM Transactions on Programming Languages and Systems,
17(2):264-292, March 1995.
-
A type system equivalent to flow analysis, with Patrick M. O'Keefe.
ACM Transactions on Programming Languages and Systems,
17(4):576-599, July 1995.
Preliminary version in Proceedings of POPL'95, 22nd Annual SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, pages 367-378, San
Francisco, California, January 1995.
-
Type inference of Self: Analysis of objects with dynamic and multiple
inheritance, with Ole Agesen and Michael I. Schwartzbach.
Software - Practice & Experience, 25(9):975-995, September
1995.
Preliminary version in Proceedings of ECOOP'93, Seventh European Conference on
Object-Oriented Programming, Springer-Verlag (LNCS 707), pages
247-267, Kaiserslautern, Germany, July 1993.
-
Strong normalization with non-structural subtyping, with Mitchell Wand and
Patrick M. O'Keefe.
Mathematical Structures in Computer Science, 5(3):419-430,
1995.
-
Efficient inference of object types.
Information and Computation, 123(2):198-209, 1995.
Preliminary version in Proceedings of LICS'94, Ninth Annual IEEE Symposium on
Logic in Computer Science, pages 186-195, Paris, France, July 1994.
-
Generating action compilers by partial evaluation, with Anders Bondorf.
Journal of Functional Programming, 6(2):269-298, 1996.
Preliminary version in Proceedings of FPCA'93, Sixth ACM Conference on
Functional Programming Languages and Computer Architecture, pages 308-317,
Copenhagen, Denmark, June 1993.
-
Constrained types and their expressiveness, with Scott Smith.
ACM Transactions on Programming Languages and Systems,
18(5):519-527, September 1996.
-
Eta-expansion does the Trick, with Olivier Danvy and Karoline Malmkjaer.
ACM Transactions on Programming Languages and Systems,
18(6):730-751, November 1996.
-
Type inference with non-structural subtyping, with Mitchell Wand and
Patrick M. O'Keefe.
Formal Aspects of Computing, 9:49-67, 1997.
-
Class-graph inference for adaptive programs.
Theory and Practice of Object Systems, 3(2):75-85, 1997.
-
Type inference with simple selftypes is NP-complete, with Trevor Jim.
Nordic Journal of Computing, 4(3):259-286, Fall 1997.
-
A new approach to compiling adaptive programs, with Boaz Patt-Shamir and
Karl Lieberherr.
Science of Computer Programming, 29(3):303-326, September 1997.
Preliminary version in Proceedings of ESOP'96, European Symposium
on Programming, Springer-Verlag (LNCS 1058), pages 280-295,
Linkoeping, Sweden, April 1996.
-
Trust in the lambda-calculus, with Peter Orbaek.
Journal of Functional Programming, 7(6):557-591, November 1997.
Preliminary version in Proceedings of SAS'95, International Static
Analysis Symposium, Springer-Verlag (LNCS 983), pages 314-330,
Glasgow, Scotland, September 1995.
-
Evolution of object behavior using context relations, with Linda Seiter and
Karl Lieberherr.
IEEE Transactions on Software Engineering.
24(1):79-92, 1998.
Preliminary version in Proceedings of ACM FSE'96, Fourth
Symposium on the Foundations of Software Engineering, San Francisco,
California, October 1996.
-
Equality-Based Flow Analysis versus Recursive Types.
ACM Transactions on Programming Languages and Systems,
20(6):1251-1264, 1998.
-
Optimal representations of polymorphic types with subtyping, with Alexander
Aiken and Edward L. Wimmers.
Higher-Order and Symbolic Computation.
12(3):1-46, October 1999.
Preliminary version in
Proceedings of TACS'97, International Symposium on Theoretical Aspects
of Computer Software, pages 47-76. Springer-Verlag (LNCS 1281),
Sendai, Japan, September 1997.
-
From polyvariant flow information to intersection and union types, with
Christina Pavlopoulou.
Journal of Functional Programming
11(3):263-317, May 2001.
Preliminary version in
Proceedings of POPL'98, 25th Annual
SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
pages 197-208, San Diego, California, January 1998.
-
Efficient and Flexible Matching of Recursive Types, with
Tian Zhao.
Information and Computation
171:364-387, 2001.
Preliminary version in
Proceedings of LICS'00,
Fifteenth Annual IEEE Symposium on Logic in Computer Science, pages 388-398,
Santa Barbara, California, June 2000.
-
CPS Transformation of Flow Information, with
Mitchell Wand.
Journal of Functional Programming,
13(5):905-923, 2003.
-
Type Inference for Record Concatenation and Subtyping, with
Tian Zhao.
Information and Computation,
189:54-86, 2004.
Preliminary version in
Proceedings of LICS'02,
IEEE Symposium on Logic in Computer Science, pages 125-136,
Copenhagen, Denmark, July 2002.
-
Compiling with code-size constraints, with Mayur Naik.
ACM Transactions on Embedded Computing Systems,
3(1):163-181, 2004.
Preliminary version in Proceedings of LCTES'02, Languages,
Compilers, and Tools for Embedded Systems joint with SCOPES'02, Software and
Compilers for Embedded Systems, pages 120-129, Berlin, Germany, June 2002.
-
Type-safe method inlining, with
Neal Glew.
Science of Computer Programming,
52:281-306, 2004.
Preliminary version in Proceedings of ECOOP'02, European
Conference on Object-Oriented Programming, pages 525-544,
Springer-Verlag (LNCS 2374), Malaga, Spain, June 2002.
-
Stack Size Analysis of Interrupt Driven Software, with Krishnendu
Chatterjee, Di Ma, Rupak Majumdar, Tian Zhao, and Thomas A. Henzinger.
Information and Computation 194(2):144-174, 2004,
special issue dedicated to Paris Kanellakis.
Preliminary version in
Proceedings of SAS'03, International Static Analysis
Symposium, pages 109-126, San Diego, June 2003.
-
Deadline analysis of interrupt-driven software,
with Dennis Brylow.
IEEE Transactions on Software Engineering, 30(10):634-655, 2004.
Preliminary version
in Proceedings of FSE'03, ACM SIGSOFT International Symposium on the
Foundations of Software Engineering joint with ESEC'03, European Software
Engineering Conference, pages 198-207, Helsinki, Finland, September 2003.
-
Automatic Discovery of Covariant Read-Only Fields, with
Tian Zhao and Trevor Jim.
ACM Transactions on Programming Languages and Systems,
27(1):126-162, January 2005.
Preliminary version in Informal Proceedings of FOOL'02,
Ninth International Workshop on
Foundations of Object-Oriented Languages, Portland, Oregon, January 2002.
-
Method inlining, dynamic class loading, and type soundness, with
Neal Glew.
In Journal of Object Technology, 4(8):33-53, 2005.
Preliminary version in the Sixth Workshop on
Formal Techniques for Java-like Programs,
Oslo, Norway, June 2004.
-
Type-based confinement, with Tian Zhao and Jan Vitek.
Journal of Functional Programming, 16(1):83-128, 2006.
Preliminary version,
entitled "Lightweight confinement for Featherweight Java",
in Proceedings of OOPSLA'03,
ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and
Applications, pages 135-148, Anaheim, California, October 2003.
-
Encapsulating objects with confined types, with
Christian Grothoff and Jan Vitek.
ACM Transactions on Programming Languages and Systems, 29(6), 2007.
Preliminary version in Proceedings of OOPSLA'01, ACM
SIGPLAN Conference on Object-Oriented Programming Systems, Languages and
Applications, pages 241-253, Tampa Bay, Florida, October 2001.
-
A type system equivalent to a model checker, with Mayur Naik.
ACM Transactions on Programming Languages and Systems 30(5), 2008.
Preliminary version in Proceedings of ESOP'05,
European Symposium on Programming,
pages 374-388, Edinburgh, Scotland, April 2005.
-
Aliased Register Allocation for Straight-line Programs is NP-complete,
with Jonathan K. Lee and Fernando Magno Quintao Pereira.
Theoretical Computer Science 407:258-273.
Preliminary version in Proceedings of ICALP'07, 34th International Colloquium on
Automata, Languages and Programming,
pages 680-691,
Wroclaw, Poland, July 2007.
-
Concurrent collections,
with Zoran Budimlic, Michael Burke, Vincent Cave, Kathleen Knobe,
Geoff Lowney, Ryan Newton, David Peixotto, Vivek Sarkar, Frank Schlimbach,
and Sagnak Tasirlar.
Scientific Programming, 18:203-217, August 2010.
-
A decoupled local memory allocator,
with Boubacar Diouf, Can Hantas, Albert Cohen, and Ozcan Ozturk.
ACM Transactions on Architecture and Code Optimization, 9(4), 2013.
-
Jones-optimal partial evaluation by specialization-safe normalization,
with Matt Brown.
Proceedings of POPL'18, SIGPLAN-SIGACT Symposium on
Principles of Programming Languages,
Los Angeles, January 2018.
Proofs and implementation.
-
Sound deadlock prediction, with Christian Gram Kalhauge.
Proceedings of OOPSLA'18, ACM SIGPLAN Conference on
Object-Oriented Programming Systems, Languages and Applications,
Boston, November 2018.
-
A formalization of Java's concurrent access modes, with John Bender.
Proceedings of the ACM on Programming Languages, 3(OOPSLA), 2019.
-
Toward a universal quantum programming language,
ACM XRDS Crossroads, 26(1), Fall 2019.
-
What is decidable about gradual types?, with Zeina Migeed.
Proceedings of the ACM on Programming Languages, 4(POPL), 2020.
-
Conferences in an era of expensive carbon, with Benjamin C. Pierce and
Michael Hicks and Crista Lopes.
Communications of the ACM, 63(3), 35-37, 2020.
-
Achieving a quantum smart workforce, with Clarice D. Aiello, D. D.
Awschalom, Hannes Bernien, Tina Brower-Thomas, Kenneth R. Brown, Todd A.
Brun, Justin R. Caram, Eric Chitambar, Rosa Di Felice, Michael F. J. Fox,
Stephan Haas, Alexander W. Holleitner, Eric R. Hudson, Jeffrey H. Hunt,
Robert Joynt, Scott Koziol, H. J. Lewandowski, Douglas T. McClure, Gina
Passante, Kristen L. Pudenz, Christopher J. K. Richardson, Jessica L.
Rosenberg, R. S. Ross, Mark Saffman, M. Singh, David W. Steuerman, Chad
Stark, Jos Thijssen, A. Nick Vamivakas, James D. Whitfield, and Benjamin M.
Zwickl.
Quantum Science and Technology, 6(3), 2021.
-
Building a quantum engineering undergraduate program, with Abraham Asfaw,
Alexandre Blais, Kenneth R. Brown, Jonathan Candelaria, Christopher Cantwell,
Lincoln D. Carr, Joshua Combes, Dripto M. Debroy, John M. Donohue, Sophia E.
Economou, Emily Edwards, Michael F. J. Fox, Steven M. Girvin, Alan Ho,
Hilary M. Hurst, Zubin Jacob, Blake R. Johnson, Ezekiel Johnston-Halperin,
Robert Joynt, Eliot Kapit, Judith Klein-Seetharaman, Martin Laforest, H. J.
Lewandowski, Theresa W. Lynn, Corey Rae H. McRae, Celia Merzbacher, Spyridon
Michalakis, Prineha Narang, William D. Oliver, David P. Pappas, Michael G.
Raymer, David J. Reilly, Mark Saffman, Thomas A. Searles, Jeffrey H. Shapiro,
and Chandralekha Singh.
IEEE Transactions on Education, 65, 2022.
Refereed Conference Papers
-
Type substitution for object-oriented programming, with Michael I.
Schwartzbach.
In Proceedings of OOPSLA/ECOOP'90, ACM SIGPLAN Fifth Annual Conference
on Object-Oriented Programming Systems, Languages and Applications; European
Conference on Object-Oriented Programming, pages 151-160, Ottawa, Canada,
October 1990.
-
What is type-safe code reuse?, with Michael I. Schwartzbach.
In Proceedings of ECOOP'91, Fifth European Conference on Object-Oriented
Programming, pages 325-341. Springer-Verlag (LNCS 512), Geneva,
Switzerland, July 1991.
-
Object-oriented type inference, with Michael I. Schwartzbach.
In Proceedings of OOPSLA'91, ACM SIGPLAN Sixth Annual Conference on
Object-Oriented Programming Systems, Languages and Applications, pages
146-161, Phoenix, Arizona, October 1991.
-
A provably correct compiler generator.
In Proceedings of ESOP'92, European Symposium on Programming, pages
418-434. Springer-Verlag (LNCS 582), Rennes, France, February 1992.
-
An automatically generated and provably correct compiler for a subset of
Ada.
In Proceedings of ICCL'92, Fourth IEEE International Conference on
Computer Languages, pages 117-126, Oakland, California, April 1992.
-
Making type inference practical, with Nicholas Oxhoj and Michael I.
Schwartzbach.
In Proceedings of ECOOP'92, Sixth European Conference on Object-Oriented
Programming, pages 329-349. Springer-Verlag (LNCS 615), Utrecht,
The Netherlands, July 1992.
-
Binding-time analysis: Abstract interpretation versus type inference, with
Michael I. Schwartzbach.
In Proceedings of ICCL'94, Fifth IEEE International Conference on
Computer Languages, pages 289-298, Toulouse, France, May 1994.
-
Comparing flow-based binding-time analyses.
In Proceedings of TAPSOFT'95, Theory and Practice of Software
Development, pages 561-574. Springer-Verlag (LNCS 915), Aarhus,
Denmark, May 1995.
-
The Essence of the Visitor Pattern, with C. Barry Jay.
In Proceedings of COMPSAC'98, 22nd Annual International Computer Software
and Applications Conference, pages 9-15,
Vienna, Austria, August 1998.
-
Program Optimization for Faster Genetic Programming,
with Bradley Lucier and Sudhakar Mamillapalli.
In Proceedings of GP'98, Genetic Programming, pages 202-207,
Madison, Wisconsin, July 1998.
-
Scalable Propagation-based Call Graph Construction Algorithms, with
Frank Tip.
In Proceedings of OOPSLA'00,
ACM SIGPLAN Conference on Object-Oriented Programming Systems,
Languages and Applications, pages 281-293,
Minneapolis, Minnesota, October 2000.
-
Experience with software watermarking, with
Sowmya Krishnaswamy, Minseok Kwon, Di Ma, Qiuyun Shao, and Yi Zhang.
In Proceedings of ACSAC'00, 16th Annual Computer Security
Applications Conference, pages 308-316,
New Orleans, Louisiana, December 2000.
-
Static Checking of Interrupt-driven Software, with
Dennis Brylow and Niels Damgaard.
In Proceedings of ICSE'01,
23rd International Conference on Software Engineering, pages 47-56,
Toronto, May 2001.
-
Efficient type matching, with
Somesh Jha and Tian Zhao.
In Proceedings of FOSSACS'02, Foundations of Software Science
and Computation Structures, pages 187-204. Springer-Verlag (LNCS 2303),
Grenoble, France, April 2002.
-
A Typed Interrupt Calculus, with Di Ma.
In Proceedings of FTRTFT'02,
7th International Symposium on Formal Techniques
in Real-Time and Fault Tolerant Systems,
pages 291-310. Springer-Verlag (LNCS 2469),
Oldenburg, Germany, September 2002.
Slides.
-
Efficient spill code for SDRAM, with V. Krishna Nandivada.
In Proceedings of CASES'03, International Conference on
Compilers, Architecture and Synthesis for Embedded Systems,
pages 24-31, San Jose, California, October 2003.
-
Timing analysis of TCP servers for surviving denial-of-service attacks,
with V. Krishna Nandivada.
In Proceedings of RTAS'05, 11th IEEE Real-Time and Embedded
Technology and Applications Symposium, pages 541-549,
San Francisco, March 2005.
-
Avrora: Scalable Sensor Network Simulation
with Exact Timing,
with Ben L. Titzer and Daniel Lee.
In Proceedings of IPSN'05, Fourth International Conference
on Information Processing in Sensor Networks, pages 477-482,
Los Angeles, April 2005.
-
Nonintrusive precision instrumentation of microcontroller software,
with Ben L. Titzer.
In Proceedings of LCTES'05, Conference on Languages, Compilers
and Tools for Embedded Systems,
pages 59-68,
Chicago, Illinois, June 2005.
-
Type-safe optimisation of plugin architectures,
with Neal Glew and Christian Grothoff.
In Proceedings of SAS'05, Static Analysis Symposium,
Springer-Verlag (LNCS 3672), pages 135-154,
London, UK, September 2005.
-
Register allocation via coloring of chordal graphs,
with Fernando Magno Quintao Pereira.
In Proceedings of APLAS'05, Asian Symposium on Programming
Languages and Systems, pages 315-329, Tsukuba, Japan, November 2005.
-
Register allocation after classical SSA elimination is NP-complete,
with Fernando Magno Quintao Pereira.
In Proceedings of FOSSACS'06, Foundations of Software Science
and Computation Structures.
Springer-Verlag (LNCS 3921), pages 79-93, Vienna, Austria, March 2006.
-
Sara: Combining stack allocation and register allocation,
with V. Krishna Nandivada.
In Proceedings of CC'06,
International Conference on Compiler Construction.
Springer-Verlag (LNCS 3923), pages 232-246, Vienna, Austria, March 2006.
-
Inference of user-defined type qualifiers and qualifier rules,
with Brian Chin and Shane Markstrum and Todd Millstein.
In Proceedings of ESOP'06, European Symposium on Programming.
Springer-Verlag (LNCS 3924), pages 264-278, Vienna, Austria, March 2006.
-
The ExoVM system for automatic VM and application reduction,
with Ben L. Titzer and Joshua Auerbach and David F. Bacon.
In Proceedings of PLDI'07, ACM SIGPLAN Conference on
Programming Language Design and Implementation, pages 352-362, San Diego, California,
June 2007.
-
A framework for end-to-end verification and evaluation of register allocators,
with V. Krishna Nandivada and Fernando Pereira.
In Proceedings of SAS'07, International Static Analysis Symposium,
pages 153-169,
Kongens Lyngby, Denmark, August 2007.
-
Vertical Object Layout and Compression for Fixed Heaps,
with Ben L. Titzer.
In Proceedings of CASES'07,
International Conference on Compilers, Architecture, and Synthesis for
Embedded Systems, pages 170-178, September 2007.
-
Register allocation by puzzle solving,
with Fernando Magno Quintao Pereira.
In Proceedings of PLDI'08, ACM SIGPLAN Conference on
Programming Language Design and Implementation, pages 216-226, Tucson, Arizona,
June 2008.
-
Constrained types for object-oriented languages,
with Vijay Saraswat and Nathaniel Nystrom, and Christian Grothoff.
In Proceedings of OOPSLA'08, ACM SIGPLAN Conference on
Object-Oriented Programming Systems, Languages and Applications,
October 2008.
To appear.
-
SSA elimination after register allocation,
with Fernando Magno Quintao Pereira.
In Proceedings of CC'09, International Conference on Compiler
Construction. Springer-Verlag (LNCS), Vienna, Austria, March 2009.
To appear.
-
Featherweight X10: a core calculus for async-finish parallelism,
with Jonathan K. Lee.
In Proceedings of PPOPP'10, 15th ACM SIGPLAN Annual Symposium on
Principles and Practice of Parallel Programming, Bangalore, India, January 2010.
-
Punctual Coalescing,
with Fernando Magno Quintao Pereira.
In Proceedings of CC'10, International Conference on Compiler
Construction. Springer-Verlag (LNCS), Paphos, Cyprus, March 2010.
To appear.
-
From OO to FPGA: Fitting round objects into square hardware?
,
with Stephen Kou.
In Proceedings of OOPSLA'10, ACM SIGPLAN Conference on
Object-Oriented Programming Systems, Languages and Applications, Reno, Nevada, 2010.
Slides.
-
The Essence of Compiling with Traces,
with Shu-yu Guo.
To appear in Proceedings of POPL'11, Annual
SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
Austin, Texas, January 2011.
-
Communicating memory transactions, with Mohsen Lesani.
In Proceedings of PPOPP'11, 16th ACM SIGPLAN Annual Symposium on
Principles and Practice of Parallel Programming, San Antonio, Texas,
February 2011.
-
Typed self-interpretation by pattern matching, with C. Barry Jay.
In Proceedings of ICFP'11,
ACM SIGPLAN International Conference on Functional Programming,
Tokyo, September 2011.
-
Testing versus static analysis of maximum stack size, with Mahdi Eslamimehr.
In Proceedings of COMPSAC'13, 37nd Annual International Computer
Software and Applications Conference, Kyoto, Japan, July 2013.
-
Proving non-opacity, with Mohsen Lesani.
In Proceedings of DISC'13,
International Symposium on Distributed Computing, Jerusalem, October 2013.
A preliminary version was presented at TRANSACT'13, Workshop on
Transactional Computing, March 2013.
-
Agnostic protocol translation for cross-domain information sharing, with
Chen Liu, Bao-Hong Shen, Soon Y. Oh, Mario Gerla, Clif Banner, and Richard
Butler.
In Proceedings of MILCOM'13, 2013.
-
Race Directed Scheduling of Concurrent Programs,
with Mahdi Eslamimehr.
In Proceedings of PPOPP'14, ACM SIGPLAN Annual Symposium on
Principles and Practice of Parallel Programming,
Orlando, Florida, February 2014.
-
Automatic Atomicity Verification for Clients of Concurrent Data Structures,
with Mohsen Lesani and Todd Millstein.
In Proceedings CAV'14, Computer Aided Verification,
Vienna, Austria, July 2014.
-
Sherlock: Scalable deadlock detection for concurrent programs,
with Mahdi Eslamimehr.
In Proceedings of FSE'14, ACM SIGSOFT International Symposium on
the Foundations of Software Engineering,
Hong Kong, November 2014.
-
Decomposing opacity,
with Mohsen Lesani.
In Proceedings of DISC'14, International Symposium on
Distributed Computing, Austin, Texas, October 2014.
-
Self-representation in Girard's System U, with Matt Brown.
Proceedings of POPL'15, SIGPLAN-SIGACT Symposium on
Principles of Programming Languages,
Mumbai, India, January 2015.
Proofs and implementation.
-
Type inference for place-oblivious objects, with Riyaz Haque.
In Proceedings of ECOOP'15,
European Conference on Object-Oriented Programming,
Prague, July 2015.
Full version.
Sixteen examples in Featherweight X10.
-
Declarative fence insertion, with John Bender and Mohsen Lesani.
In Proceedings of OOPSLA'15, ACM SIGPLAN Conference on
Object-Oriented Programming Systems, Languages and Applications,
Pittsburgh, Pennsylvania, October 2015.
-
Retargetable communication for distributed programs,
with Oren Freiberg and Mahdi Eslamimehr.
In Proceedings of QoSA'16, ACM SIGSOFT Conference on Quality of
Software Architectures, Venice, Italy, April 2016.
-
Breaking through the Normalization Barrier:
A Self-interpreter for F-omega, with Matt Brown.
Proceedings of POPL'16, SIGPLAN-SIGACT Symposium on
Principles of Programming Languages,
St. Petersburg, Florida, January 2016.
Proofs and implementation.
-
Typed self-evaluation via intensional type functions, with Matt Brown.
Proceedings of POPL'17, SIGPLAN-SIGACT Symposium on
Principles of Programming Languages,
Paris, January 2017.
Proofs and implementation.
-
Binary Reduction of Dependency Graphs, with Christian Gram Kalhauge.
In Proceedings of FSE'19, ACM SIGSOFT International Symposium on
the Foundations of Software Engineering,
Tallinn, Estonia, Sep 2019.
-
Low-overhead deadlock prediction, with Yan Cai and Ruijie Meng.
In Proceedings of ICSE'20, 23rd International Conference on
Software Engineering, pages 1298-1309, 2020.
-
Quantum abstract interpretation, with Nengkun Yu.
In Proceedings of PLDI'21, ACM SIGPLAN Conference on
Programming Language Design and Implementation, June 2021.
-
Logical bytecode reduction, with Christian Gram Kalhauge.
In Proceedings of PLDI'21, ACM SIGPLAN Conference on
Programming Language Design and Implementation, June 2021.
-
Sound and efficient concurrency bug prediction, with Yan Cai, Hao Yun and
Jinqiu Wang and Lei Qiao.
In Proceedings of FSE'21, ACM SIGSOFT International Symposium on
the Foundations of Software Engineering, 2021.
-
Quartz: Superoptimization of Quantum Circuits,
with Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing,
Auguste Hirth, Henry Ma, Alex Aiken, Umut A. Acar, Zhihao Jia.
In Proceedings of PLDI'22, ACM SIGPLAN Conference on
Programming Language Design and Implementation,
San Diego, California, June 2022.
Arxiv version.
-
Striking a balance: Pruning false-positives from static call graphs,
with Akshay Utture and Shuyang Liu and Christian Gram Kalhauge.
In Proceedings of ICSE'22, 23rd International Conference on
Software Engineering, pages 2043-2055, 2022.
-
Fast and precise application code analysis using a partial library,
with Akshay Utture.
In Proceedings of ICSE'22, 23rd International Conference on
Software Engineering, pages 934-945, 2022.
-
Compiling volatile correctly in Java, with Shuyang Liu and John Bender.
In Proceedings of ECOOP'22, European Conference on
Object-Oriented Programming, Prague, Jul 2022.
Refereed Survey Papers
Other Papers
-
Three discussions on object-oriented typing, with Michael I. Schwartzbach.
ACM SIGPLAN OOPS Messenger, 3(2):31-38, 1992.
-
Layout construction: A case study in algorithm engineering, with
Gudmund Skovbjerg Frandsen, Erik Meineche Schmidt, and Steen Sjogaard.
Technical Report DAIMI PB-450, Computer Science Department, Aarhus
University, August 1993.
-
Foundations of object-oriented languages, with Andrew Black.
ACM SIGPLAN Notices, 29(3):3-11, 1994.
-
Type inference in systems of recursive types with subtyping, with
Trevor Jim.
Manuscript, 1999.
-
Eta-redexes in partial evaluation.
In John Hatcliff, Torben Mogensen, and Peter Thiemann, editors,
Partial Evaluation: Practice and Theory, pages 356-366.
Springer-Verlag, 1999.
-
Reducing loads and stores in stack architectures, with
Thomas VanDrunen and Antony L. Hosking.
Manuscript, 2000.
-
Type-based analysis and applications,
In Proceedings of PASTE'01, ACM SIGPLAN/SIGSOFT Workshop on
Program Analysis for Software Tools,
pages 20-27, Snowbird, Utah, June 2001.
-
Reverse engineering of real-time assembly code, with
Matthew Wallace.
Manuscript, 2002.
-
Teaching reviewing to graduate students, with Scott J. Baxter.
Communications of the ACM, 45(12):22-24, December 2002.
(Extended version).
-
ILP-based Resource-aware Compilation,
with Mayur Naik.
In Ahmed Jerraya and Wayne Wolf, editors, Multiprocessor Systems-on-Chips,
Chapter 12.
Elsevier, 2004.
-
Programming languages.
In Richard C. Dorf, editor,
The Engineering Handbook, chapter 145.
CRC Press, 2004.
-
Visitor-Oriented Programming, with
Thomas VanDrunen.
Presented at the Eleventh International Workshop on
Foundations of Object-Oriented Languages,
Venice, Italy, January 2004.
(slides)
-
Enabling detailed modeling and analysis of sensor networks,
with Olaf Landsiedel and Klaus Wehrle and Ben L. Titzer.
In Praxis der Informationsverarbeitung und Kommunikation
28(2):10-15, 2005.
-
Type systems: Advances and applications,
with Todd Millstein.
In Y. N. Srikant and Priti Shankar, editors,
The Compiler Design Handbook, chapter 9. CRC Press, 2007.
-
Flow analysis of an intermediate language for object-oriented languages,
with Neal Glew and Ben L. Titzer.
Manuscript, 2005.
-
A Declarative Approach to Generating Machine Code Tools,
with Ben L. Titzer and Jonathan K. Lee.
Manuscript, 2006.
-
Overloading is NP-complete,
a tutorial dedicated to Dexter Kozen.
In Logic and Program Semantics, pages 204-218,
Springer, LNCS 7230, 2012.
-
Efficient May Happen in Parallel Analysis for Async-Finish Parallelism,
with Jonathan K. Lee, Rupak Majumdar, and Hong Hong.
Proceedings of SAS'12, International Static Analysis Symposium, 2012.
-
Write-observation and read-preservation TM correctness invariants,
with Mohsen Lesani.
In 5th Workshop on the Theory of Transactional Memory,
Jerusalem, October 2013.
-
NJR: a normalized Java resource,
with Cristina Lopes.
Proceedings of SOAP'18, International Workshop on the
State Of the Art in Program Analysis, July 2018.
-
Toward a universal quantum programming language.
ACM XRDS Crossroads 26:1, Fall 2019.
Short version on the SIGPLAN blog.
Other Manuscripts
-
Correctness of ILP-based register allocation, with Mayur Naik.
Manuscript, 2004.
-
Efficient type-2 puzzle solving, with Siddharth Tiwary.
Manuscript, 2009.