Harry Mairson
Degrees
Stanford University, Ph.D.Yale University, B.A.
Expertise
Logic in computer science. Lambda calculus and functional programming. Software for classical string instrument design.Profile
Please visit my new faculty profile page.
I have worked on various problems related to type systems for programming languages, in particular, analyzing the computational resources needed for different kinds of optimizations (type inference, optimal reduction, intersection types and flow analysis, static analysis). This work has been motivated by many ideas from linear logic. More recently I am interested in developing a domain-specific programming language for string instrument design, where the language uses the same constructional vernacular found in the seventeenth-century methods, only with a more refined and specific computational interpretation. Webpage
Courses Taught
| COSI | 29a | Discrete Structures |
| COSI | 121b | Structure and Interpretation of Computer Programs |
| COSI | 190a | Introduction to Programming Language Theory |
Awards and Honors
SIGPLAN Research Highlight Award (for "Functional Geometry and the Traité de Lutherie", ICFP 2013) (2014)
Professeur Invité, Institut de Mathematiques de Luminy, Université de Marseille (2009)
2007 Most Influential ICFP Paper Award, for "Optimality and Inefficiency: What Isn't a Cost Model of the Lambda Calculus?" (with Julia Lawall), presented at the 1996 ACM International Conference on Functional Programming. (2007)
Associate Editor, Logical Methods in Computer Science (2004)
CNRS Chercheur Invité, Equipe Logique de la Programmation, Institut de Mathématiques de Luminy, Marseille (2004)
Invited Speaker, 5th Annual Workshop on Implicit Computational Complexity, Ottawa, Canada (sponsored by the IEEE Symposium on Logic in Computer Science), June (2003)
Invited Speaker, 8th International Conference on Functional Programming, Uppsala, Sweden (sponsored by the Association for Computing Machinery), August (2003)
Invited Speaker, 23rd Conference on Foundations of Software Technology and Theoretical Computer Science, Indian Institute of Technology, Kanpur (sponsored by the Indian Association for Research in Computing Science), December (2002)
Editorial Board, Higher-Order and Symbolic Computation (2000)
Associate Editor, Information and Computation (1996 - 2008)
Marver and Sheva Bernstein Faculty Fellowship (1991 - 1992)
Scholarship
Mairson, Harry. "Project Luthier." The Strad 72-79..
Mairson, Harry. http://www.cs.brandeis.edu/~mairson/TDL
Mairson, Harry. "Liberté de parole à l'université." Faculté des Sciences de Luminy, Université de Marseille
Mairson, Harry (editor, with O. Danvy, F. Henglein, and A. Pettorossi). Automatic Program Development: A Tribute to Robert Paige. Springer, 2008.
Mairson, Harry (with David Van Horn). "Deciding kCFA is complete for EXPTIME." ACM International Conference on Functional Programming, Victoria, British Columbia, Canada. 2008.
Mairson, Harry. "Flow analysis, linearity, and PTIME." 15th International Static Analysis Symposium (SAS 2008), Valencia, Spain. 16-18 July, 2008.
Mairson, Harry. "Imagining a Civil University: Its Necessity and Insufficiency." 2008 National Hillel Summit: Imagining a Civil Society---the University and the Jewish Community. Washington, DC. March 2008.
Mairson, Harry. "Linear Logic and the Complexity of Flow Analysis." Workshop on Implicit Computational Complexity, University of Paris (Villetaneuse). 2008.
Mairson, Harry. "MLL normalization and transitive closure: circuits, complexity, and Euler tours." GEOCAL (Geometry of Calculation): Implicit Computational Complexity. Institut de Mathematique de Luminy, Marseille. February, 2006.
Mairson, Harry. Relating Complexity and Precision in Control Flow Analysis. Proc. of ACM International Conference on Functional Programming. Freiburg, Germany: 2007.
Mairson, Harry. "Proofnets and Paths in Constructive Classical Logic: Too Old, Too New." GEOCAL (Geometry of Calculation): Geometry of Interaction. Institut de Mathematiques de Luminy, Marseille. February, 2006.
Mairson,Harry. "Linear lambda calculus and PTIME-completeness." Journal of Functional Programming (2005): 623-633.
Mairson,Harry (with Peter Møller Neergaard). "Types, Potency, and Idempotency: why nonlinearity and amnesia make a type system work." ACM International Conference on Functional Programming (2004): 138-149.
Mairson, Harry and Xavier Rival. Proofnets and context semantics for the additives. Proc. of Computer Science Logic (CSL). Edinburgh: Springer-Verlag, 2002.
Mairson,Harry. From Hilbert space to Dilbert space: context semantics made simple. Proc. of Proceedings, FSTTCS Conference: Lecture Notes in Computer Science. 2002.
Mairson,Harry (with Andrea Asperti). "Parallel beta reduction is not elementary recursive." Information and Computation 170. 1 (2001): 49-80.
Mairson, Harry and Julia Lawall. "Sharing continuations: proofnets for languages with explicit control." European Symposium on Programming (ESOP), 2000.