Andrew Tolmach

Professor
Department of Computer Science
Portland State University

Ph.D., Computer Science, Princeton University, 1992.

Email:	tolmach@pdx.edu
Office:	120-23 FAB
Phone:	(503) 725-5492

Office hours: by appointment, on zoom or in person (send email).

Current Courses (Fall 2024)

CS558 Programming Languages

Brief Biography

My research interests are in programming languages, verification, compilers, tools, and applications, with a focus on high-assurance software environments. I am currently investigating the use of novel hardware-level tagging mechanisms to perform security monitoring, under the generous support of the NSF. I also collaborate with the TU Delft Programming Languages Group on the Language Designer's Workbench project. My past publications, mostly about functional languages, include work on debugger implementation, garbage collection, compilation, integration with logic languages, and lazy functional algorithms. I teach courses in programming languages, compilers, semantics, and theorem proving.

Some Publications

"SECOMP: Formally Secure Compilation of Compartmentalized C Programs" (joint with Jérémy Thibault, Roberto Blanco, Dongjae Lee, Sven Argo, Arthur Azevedo de Amorim, Aïna Linn Georges, and Cătălin Hriţcu), CCS 24, October 2024.

"Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model" (joint with Chris Chhak and Sean Anderson), ITP 24, September 2024.

"Flexible Runtime Security Enforcement with Tagged C" (joint with Sean Anderson and Allison Naaktgeboren), RV 23, October 2023.

"Formalizing Stack Safety as a Security Property" (joint with Sean Anderson, Roberto Blanco, Leonidas Lampropoulos, and Benjamin C. Pierce), CSF 2023, July 2023.

"Towards Formally Verified Compilation of Tag-Based Policy Enforcement" (joint with CHR Chhak and Sean Anderson), CPP 2021, January 2021.

"Scopes and Frames Improve Meta-interpreter Specialization" (joint with Vlad Vergu and Eelco Visser), ECOOP 2019, London, July 2019.

"When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise" (joint with Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Cătălin Hriţcu, Théo Laurent, Benjamin C. Pierce, and Marco Stronati), CCS 2018, Toronto, October 2018.

"Intrinsically-typed Definitional Interpreters for Imperative Languages" (joint with Casper Bach Poulsen, Arjen Rouvoet, Robbert Krebbers, and Eelco Visser), POPL 2018, Los Angeles, Jan. 2018.

"A Verified Information-Flow Architecture" (joint with Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, and Randy Pollack), Journal of Computer Security, 24(6), 2016.

"Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics" (joint with Casper Bach Poulsen, Pierre Neron, and Eelco Visser), ECOOP 2016, Rome, July 2016.

"A Domain-Specific Constraint Language for Static Semantic Analysis based on Scope Graphs" (joint with Hendrik van Antwerpen, Pierre Neron, Eelco Visser, and Guido Wachsmuth), PEPM 2016, St. Petersburg, FL, January 2016.

"Micro-Policies: Formally Verified, Tag-Based Security Monitors" (joint with Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hriţcu, Benjamin C. Pierce, and Antal Spector-Zabusky), IEEE Security and Privacy 2015, San Jose, May 2015. (Associated Coq code.)

"A Theory of Name Resolution" (joint with Pierre Neron, Eelco Visser, and Guido Wachsmuth), ESOP 2015, London, April 2015. (EAPLS best paper award for ETAPS 2015.) (Extended technical report)

"Static Conflict Detection for a Policy Language" (joint with Alix Trieu and Robert Dockins), JFLA 2015, Val d'Ajol, France, January 2015.

"SUPPL: A Flexible Language for Policies" (joint with Robert Dockins), APLAS 2014, Singapore, November 2014. (Related software.)

"A Language Designer's Workbench: A One-Stop-Shop for Implementation and Verification of Language Designs" (joint with Eelco Visser, Guido Wachsmuth, Pierre Neron, Vlad Vergu, Augusto Passalaqua, and Gabriël Konat), Onward! 2014, Portland, OR, October 2014.

"A Certified Framework for Compiling and Executing Garbage-collected Languages" (joint with Andrew McCreight and Tim Chevalier), Proc. 2010 ACM International Conference on Functional Programming, Baltimore, Sept. 2010.

"Lightweight Concurrency Primitives for GHC" (joint with Peng Li, Simon Marlow, and Simon Peyton Jones), Proc. 2007 Haskell Workshop, Freiburg, Germany, Sept. 2007.

"A Principled Approach to Operating System Construction in Haskell" (joint with Thomas Hallgren, Mark P. Jones, and Rebekah Leslie), Proc. 2005 ACM International Conference on Functional Programming, Tallinn, Estonia, Sept. 2005.

"A Virtual Machine for Functional Logic Computations" (joint with Sergio Antoy, Michael Hanus, and Jimeng Liu), Proc. 16th International Workshop on Implementation and Application of Functional Languages (IFL 2004).

"Implementing Functional Logic Languages Using Multiple Threads and Stores" (joint with Sergio Antoy and Marius Nita), Proc. 2004 ACM International Conference on Functional Programming, Snowbird, Utah, Sept. 2004, pp. 90-102.

"A Monadic Semantics for Core Curry" (joint with Sergio Antoy), Proc. Workshop on Functional and (Constraint) Logic Programming, Valencia, Spain, June 2003, ENTCS vol. 86, no 3. (Associated Haskell code).

"Playing by the Rules: Rewriting as an Optimization Technique in GHC" (joint with Simon Peyton Jones and Tony Hoare), Proc. 2001 Haskell Workshop, Florence, Italy, Sept. 2001, pp. 203-233.

"Modular Lazy Search for Constraint Satisfaction Problems" (joint with Thomas Nordin), Journal of Functional Programming, 11(5), pp. 557-587.,Sept. 2001. (Associated Haskell code.)

"Typed Higher-order Narrowing without Higher-order Strategies" (joint with Sergio Antoy), Proc. FLOPS'99, Tsukuba, Japan, November 1999, pp. 335-352.

"Interface-Directed Partial Evaluation" (joint with Zine-el-Abidine Benaissa), OGI Technical Report #99-10, September 1999.

"Building Program Optimizers with Rewriting Strategies" (joint with Eelco Visser and Zine-el-Abidine Benaissa), Proc. 1998 International Conference on Functional Programming, September 1998, pp. 13-26.

"Optimizing ML Using a Hierarchy of Monadic Types", Types in Compilation '98 Workshop, Kyoto, Japan, March 1998, LNCS v. 1473, pp. 97-113.

"From ML to Ada: Strongly-typed Language Interoperability via Source Translation", (joint with D. Oliva). Journal of Functional Programming , 8(4),367-412, July 1998.

"Bridging the gulf: a common intermediate language for ML and Haskell," (joint with S. Peyton Jones, J. Launchbury, and M. Shields). POPL '98. With an unfortunate corrigendum.

"Combining Closure Conversion with Closure Analysis using Algebraic Types", presented at Types in Compilation workshop, Amsterdam, June 8, 1997.

"A Debugger for Standard ML", (joint with A. Appel), Journal of Functional Programming, 5(2),155-200, April 1995.

"Tag-free Garbage Collection Using Explicit Type Parameters," Proceedings 1994 ACM Conference on Lisp and Functional Programming, June, 1994, published as LISP Pointers, 7(3):1-11, July-Sep. 1994.

"Procs and Locks: A Portable Multiprocessing Platform for Standard ML of New Jersey," (joint with J.G. Morrisett), 4th ACM Symposium on Principles and Practices of Parallel Programming, May 1993, pp. 198-207.

Debugging Standard ML, Ph. D. thesis, Princeton University, Oct. 1992.

"Debuggable concurrency extensions for Standard ML," (joint with A. Appel), Proceedings ACM/ONR Workshop on Parallel and Distributed Debugging, May 1991, pp. 120-131.

"Using Compact Data Representations for Languages Based on Catamorphisms," (joint with L. Fegaras), OGI Technical Report #95-025.

Old Course Materials

CS410P/510 Programming Language Semantics, Spring 2024.

CS410P/510 Programming Language Compilation, Winter 2024.

CS558 Programming Languages, Fall 2023.

CS358 Principles of Programming Languages, Spring 2023.

CS410P/510 Programming Language Compilation, Fall 2022.

CS578 Programming Language Semantics, Spring 2022.

CS558 Programming Languages, Winter 2022.

CS558 Programming Languages, Fall 2021.

CS410/510 Compilers and Interpreters, Spring 2021.

CS410/510 Theorem Proving and Program Verification, Winter 2021.

CS558 Programming Languages, Winter 2021.

CS558 Programming Languages, Fall 2020.

CS320 Principles of Programming Languages, Fall 2019.

CS320 Principles of Programming Languages, Winter 2019.

CS510 Theorem Proving and Program Verification, Fall 2018.

CS577/677 Modern Language Processors, Spring 2018.

CS457/557 Functional Languages, Spring 2018.

CS558 Programming Languages, Winter 2018.

CS558 Programming Languages, Fall 2017.

CS584/684 Algorithm Analysis and Design, Spring 2017.

CS558 Programming Languages, Winter 2017.

CS558 Programming Languages, Fall 2016.

CS584/684 Algorithm Analysis and Design, Spring 2016.

CS410/510 Practical Specification and Verification, Winter 2016.

CS558 Programming Languages, Fall 2015.

CS510 Advanced Programming Language Implementation, Spring 2014.

CS410/510 Computer-Assisted Theorem Proving, Spring 2013.

CS558 Programming Languages, Winter 2013.

CS491/591 Introduction to Computer Security, Fall 2012.

CS322 Languages and Compiler Design II, Spring 2012.

CS321 Languages and Compiler Design I, Winter 2012.

CS577 Modern Language Processors, Spring 2011.

CS322 Languages and Compiler Design II, Winter 2011.

CS321 Languages and Compiler Design I, Fall 2010.

CS578 Programming Language Semantics, Spring 2010.

CS558 Programming Languages, Winter 2010.

CS311 Computational Structures, Fall 2009.

CS311 Computational Structures, Spring 2009.

CS410/510 Automated Deduction, Fall 2008.

CS311 Computational Structures, Fall 2008.

CS577 Modern Language Processors, Spring 2008.

CS558 Programming Languages, Winter 2008.

CS510 Semantics and Types, Winter 2008.

CS577 Modern Language Processors, Spring 2006

CS558 Programming Languages, Winter 2006.

CS457/557 Functional Languages, Fall 2005.

CS510/610 Semantics and Types, Fall 2005.

CS577 Modern Language Processors, Spring 2005.

CS322 Languages and Compiler Design II, Winter 2005.

CS321 Languages and Compiler Design I, Fall 2004.

CS510/610 Semantics and Types, Spring 2004.

CS558 Programming Languages, Winter 2004.

CS577 Modern Language Processors, Winter 2004.

CS558 Programming Languages, Fall 2003.

CS457/557 Functional Languages, Spring 2003.

CS510 Theory and Practice of Functional Logic Programming, Winter 2003.

CS322 Languages and Compiler Design II, Winter 2003.

CS321 Languages and Compiler Design I, Fall 2002.

CS577 Compiler Construction, Spring 2002.

CS558 Programming Languages, Winter 2002.

CS558 Programming Languages, Fall 2001.

CS410/510 Compiling Advanced Languages, Spring 2000.

CS201 (Section 001) Computer Architecture, Winter 2000.

CS302 Languages and Compiler Design II, Spring 1999.

CS457/557 Functional Languages, Spring 1999.

CS301 Languages and Compiler Design I, Winter 1999.

CS558 Programming Languages, Fall 1998.

CS302 Languages and Compiler Design II, Spring 1998.

CS510JIP Understanding Java Implementation, Winter 1998.

CS558 Programming Languages, Fall 1997.

CS457/557 Functional Languages, Spring 1997.

CS302 Languages and Compiler Design II, Winter 1997.

CS558 Programming Languages, Fall 1996.

CS510 Compiling Functional Languages, Spring 1996.

CS458/558 Programming Languages, Fall 1994.

CS510 Compiling Functional Languages, Spring 1994.

Introductory Lecture on Functional Programming,Tektronix, August 1994.

Contact

Andrew Tolmach
Department of Computer Science
Portland State University
P.O. Box 751
Portland, OR 97207-0751

Fedex, UPS, etc.:
Computer Science Department
Rm. 120-23 FAB
1900 SW 4th Avenue
Portland, OR 97201

Phone: (503) 725-5492
FAX:   (503) 725-3211

Personal Links

My wife, Alycia Allen Tolmach, has a fiber art and surface design studio called Alyen Creations.

I sing with the Portland Bach Cantata Choir.

Last updated 20 September 2021.