Dan Grossman's Publications

Recent Work

• Transactional Events for ML. Draft
  Laura Effinger-Dean, Matthew Kehrt, Dan Grossman.
  13th ACM International Conference on Functional Programming, Victoria, Canada, September, 2008. To appear.
  The equivalence proof and Caml implementation are here.

Journal Publications

• Safe Manual Memory Management in Cyclone. This version is prior to copy-editing.
  Nikhil Swamy, Michael Hicks, Greg Morrisett, Dan Grossman, Trevor Jim.
  Science of Computer Programming, 62(2), pages 122–144, October 2006.
  
  
• Quantified Types in an Imperative Language. This version is prior to copy-editing.
  Dan Grossman.
  ACM Transactions on Programming Languages and Systems, 28(3), pages 429–475, May 2006.
  
  
• Compiling for Template-Based Run-Time Code Generation.
  Frederick Smith, Dan Grossman, Greg Morrisett, Luke Hornof, Trevor Jim.
  Journal of Functional Programming, 13(3), pages 677–708, May 2003.
  
  
• Syntactic Type Abstraction.
  Dan Grossman, Greg Morrisett, Steve Zdancewic.
  ACM Transactions on Programming Languages and Systems, 22(6), pages 1037–1080, November 2000.
  This work extends, "Principals in Programming Languages: A Syntactic Proof Technique."

Highly Selective Conference Publications

• Automatic Transformation of Bit-Level C Code to Support Multiple Equivalent Data Layouts.
  Marius Nita, Dan Grossman.
  International Conference on Compiler Construction, pages 85–99, Budapest, Hungary, March–April 2008.
  
  
• High-Level Small-Step Operational Semantics for Transactions.
  Katherine F. Moore, Dan Grossman.
  The 35th Annual ACM Symposium on Principles of Programming Languages, pages 51–62, San Francisco, CA, January 2008.
  Technical companion with full proofs
  Note: An earlier version was presented at the 2nd ACM SIGPLAN Workshop on Transactional Computing, August 2007.
  
  
• A Theory of Platform-Dependent Low-Level Software.
  Marius Nita, Dan Grossman, Craig Chambers.
  The 35th Annual ACM Symposium on Principles of Programming Languages, pages 209–220, San Francisco, CA, January 2008.
  Technical companion with full proofs
  
  
• The Transactional Memory / Garbage Collection Analogy.
  Dan Grossman.
  ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (Essays Track), Montreal, Canada, pages 695–706, October 2007.
  
  
• Enforcing Isolation and Ordering in STM.
  Tatiana Shpeisman, Vijay Menon, Ali-Reza Adl-Tabatabai, Steve Balensiefer, Dan Grossman, Richard Hudson, Katherine F. Moore, Bratin Saha.
  ACM Conference on Programming Language Design and Implementation, pages 78–88, San Diego, CA, June 2007.
  
  
• Searching for Type-Error Messages.
  Benjamin Lerner, Matthew Flower, Dan Grossman, Craig Chambers.
  ACM Conference on Programming Language Design and Implementation, pages 425–434, San Diego, CA, June 2007.
  
  
• Automatically Inferring Structural Changes for Matching Across Program Versions
  Miryung Kim, David Notkin, Dan Grossman.
  29th International Conference on Software Engineering, pages 333–343, Minneapolis, MN, May 2007.
  
  
• Preventing Format-String Attacks via Automatic and Efficient Dynamic Checking.
  Michael F. Ringenburg, Dan Grossman.
  12th ACM Conference on Computer and Communications Security, pages 354–363, Alexandria, VA, November 2005.
  
  
• AtomCaml: First-Class Atomicity via Rollback.
  Michael F. Ringenburg, Dan Grossman.
  10th ACM International Conference on Functional Programming, pages 92–104, Tallinn, Estonia, September 2005.
  
  
• Region-Based Memory Management in Cyclone.
  Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, James Cheney.
  ACM Conference on Programming Language Design and Implementation, pages 282–293, Berlin, Germany, June, 2002.
  Associated Technical Report: Cornell CS Technical Report 2001-1856
  
  
• Cyclone: A safe dialect of C.
  Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney, Yanling Wang.
  USENIX Annual Technical Conference, pages 275–288, Monterey, CA, June 2002.
  
  
• Existential Types for Imperative Languages.
  Dan Grossman.
  11th European Symposium on Programming, volume 2305 of Lecture Notes in Computer Science, pages 21–35, Grenoble, France, April 2002. © Springer-Verlag.
  Associated Technical Report: Cornell CS Technical Report 2001-1854
  
  
• Principals in Programming Languages: A Syntactic Proof Technique.
  Steve Zdancewic, Dan Grossman, Greg Morrisett.
  4th ACM International Conference on Functional Programming, pages 197–207, Paris, France, Septempter 1999.
  "Syntactic Type Abstraction" is a revised and extended version.

Other Conference and Workshop Publications

• Software Transactions Meet First-Class Continuations.
  Aaron Kimball, Dan Grossman.
  ACM SIGPLAN Workshop on Scheme and Functional Programming, Freiburg, Germany, September 2007.
  
  
• Atomicity via Source-to-Source Translation.
  Benjamin Hindman, Dan Grossman.
  ACM SIGPLAN Workshop on Memory Systems Performance and Correctness, pages 82–91, San Jose, CA, October 2006.
  Extended description: UW-CSE Technical Report 2006-05-01, May 2006
  
  
• What Do High-Level Memory Models Mean for Transactions?.
  Dan Grossman, Jeremy Manson, William Pugh.
  ACM SIGPLAN Workshop on Memory Systems Performance and Correctness, pages 62–69, San Jose, CA, October 2006.
  
  
• Seminal: Searching for ML Type-Error Messages.
  Benjamin Lerner, Dan Grossman, Craig Chambers.
  ACM SIGPLAN Workshop on ML, pages 63–73, Portland, OR, September 2006.
  
  
• Types for Describing Coordinated Data Structures.
  Michael F. Ringenburg, Dan Grossman.
  ACM SIGPLAN Workshop on Types in Language Design and Implementation, pages 25–36, Long Beach, CA, January 2005.
  
  
• Experience With Safe Manual Memory-Management in Cyclone.
  Michael Hicks, Greg Morrisett, Dan Grossman, Trevor Jim.
  International Symposium on Memory Management, pages 73–84, Vancouver, Canada, October 2004.
  
  
• Type-Safe Multithreading in Cyclone.
  Dan Grossman.
  ACM SIGPLAN Workshop on Types in Language Design and Implementation, pages 13–25, New Orleans, LA, January 2003.
  
  
• Scalable Certification for Typed Assembly Language.
  Dan Grossman, Greg Morrisett.
  3rd International Workshop on Types in Compilation, volume 2071 of Lecture Notes in Computer Science, pages 117–145, Montreal, Canada, September 2000. © Springer-Verlag.
  
  
• TALx86: A Realistic Typed Assembly Language.
  Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, Steve Zdancewic.
  ACM Workshop on Compiler Support for System Software, pages 25–35, Atlanta, GA, May 1999.
  
  
• JDuck: Building a Software Engineering Tool in Java as a CS2 Project.
  Michael Godfrey, Dan Grossman.
  30th SIGCSE Technical Symposium on Computer Science Education, pages 48–52, New Orleans, LA, March 1999.

Other Publications

• Cyclone: a Type-safe Dialect of C.
  Dan Grossman, Michael Hicks, Greg Morrisett, Trevor Jim.
  C/C++ Users Journal, 23(1), January 2005.
  
  
• Safe Programming at the C Level of Abstraction.
  Dan Grossman.
  PhD thesis, Cornell University, August 2003.