Paul Downen

Paul Downen

Assistant Professor

College
Kennedy College of Sciences
Department
Miner School of Computer & Information Sciences
Phone
978-934-3674
Office
Dandeneau Hall, Room 301
Email
Paul_Downen@uml.edu
Links

Expertise

Programming Languages, Logic, Compilation, Formal Methods

Research Interests

My general research interests are in the logic, semantics, and implementation of programming languages. In particular, I am interested in using logic to help design and verify that software systems and their compilation is efficient, correct, safe, and secure.

My primary research lies in the intersection of logic and programming, known as the Curry-Howard correspondence or proofs as programs paradigm. This area is widely known for its ability to help with verifying the correctness of software and making programs easier to write. While undoubtedly true, logic also helps tackle another programming challenge: efficiently implementing programs in real machines. It turns out that the same tools which help us humans understand and reason about what programs do, also helps computers analyze and optimize its executable code.

My work is based on a logical foundation for programs and computation that revolves around the idea of duality: every action has an equal and opposite reaction. The object-oriented and functional programming paradigms are duals. The data flowing through your program is dual to the machine's jumps between lines of code that occur during its execution. I am working to implement some of these ideas in the Glasgow Haskell Compiler in order to help optimize functional programs, and bridge the gap between the ease of programming in high-level languages versus the efficient performance of low-level systems languages.

Education

  • Ph.D. in Computer Science (2017), University of Oregon - Eugene, OR
    Dissertation/Thesis Title: Sequent Calculus: A Logic and a Language for Computation and Duality
  • B.S. Computer Science (2010), Lawrence Technological University - Southfield, MI
  • B.S. Computer Engineering (2010), Lawrence Technological University - Southfield, MI

Biosketch

Paul Downen is an assistant professor at the University of Massachusetts Lowell, joining the Miner School of Computer & Information Sciences in 2021. He received a Ph.D. from the University of Oregon's Computer and Information Science Department, and has been a visiting researcher at INRIA and Microsoft Research. His research centers on using logic to improve the efficiency, correctness, and safety of programs and their compilation. Paul's thesis - for which he was awarded the University's Doctoral Research Fellowship - explored applications of proof theory towards the design and implementation of programming languages, and for verifying programs. Applications of his work have been implemented in the Glasgow Haskell Compiler, where it is being used to improve the optimization of real-world functional programs. His research appears in top conferences and journals for programming languages, such as the Journal of Functional Programming, Logical Methods in Computer Science, Fundamenta Informaticae, PLDI, ICFP, and ESOP, and has received best paper awards. These articles include a series of tutorials focused on disseminating theoretical material to a wider community, which prompted the Journal of Functional Programming to create a category of similar "tutorial" articles inspired by Paul's work. In addition to organizing the Oregon Programming Languages Summer School for several years, Paul has been instrumental in its outreach to a more diverse audience - including young students and professionals from industry - by introducing a "Foundations" lecture series accompanying OPLSS.

Selected Awards and Honors

  • Best Paper Award (2017), Programming Languages Design and Implementation
  • Oregon Doctoral Research Fellowship (2017) , University of Oregon
  • Best Paper Award nomination (2012), European Joint Conferences on Theory and Practice of Software

Selected Publications

  • Paul Downen and Zena M. Ariola. (2021). Duality In Action. In Formal Structures for Computation and Deduction (FSCD).
  • Paul Downen, Zena M. Ariola, Simon Peyton Jones, and Richard A. Eisenberg. (2020). Kinds Are Calling Conventions. In International Conference on Functional Programming (ICFP).
  • Paul Downen and Zena M. Ariola. (2020). Compiling With Classical Connectives. Logical Methods in Computer Science, 16(3).
  • Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. (2019). Codata In Action. In European Symposium on Programming (ESOP).
  • Paul Downen, Zena M. Ariola, and Silvia Ghilezan. (2019). The Duality of Classical Intersection and Union Types. Fundamenta Informaticae, 170.
  • Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. (2019). Making a Faster Curry with Extensional Types. In Haskell Symposium.
  • Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola. (2019). Abstracting Models of Strong Normalization for Classical Calculi. Journal of Logical and Algebraic Methods in Programming.
  • Paul Downen and Zena M. Ariola. (2018). A Tutorial on Computational Classical Logic and the Sequent Calculus. Journal of Functional Programming, 28 e3.
  • Paul Downen and Zena M. Ariola. (2018). Beyond Polarity: Towards a Multi-Discipline Intermediate Language with Sharing. In Computer Science Logic (CSL).
  • Luke Maurer, Paul Downen, Zena M. Ariola, and Simon Peyton Jones. (2017). Compiling Without Continuations. In Programming Language Design and Implementation, Barcelona, Spain (PLDI).
  • Philip Johnson-Freyd, Paul Downen, and Zena M. Ariola. (2017). Call-by-Name Extensionality and Confluence. Journal of Functional Programming, 27 e12.
  • Paul Downen, Luke Maurer, Zena Ariola, and Simon Peyton Jones. (2016). Sequent Calculus As a Compiler Intermediate language. In International Conference on Functional Programming (ICFP).
  • Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola. (2015). Structures For Structural Recursion. In International Conference on Functional Programming (ICFP).
  • Paul Downen and Zena M. Ariola. (2014). The Duality of Construction. In European Symposium on Programming (ESOP).
  • Paul Downen and Zena M. Ariola. (2014). Compositional Semantics For Composable Continuations: From Abortive To Delimited Control. In International Conference on Functional Programming (ICFP).
  • Paul Downen and Zena M. Ariola. (2014). Delimited Control and Computational Effects. Journal of Functional Programming, 24.
  • Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, and Alexis Saurin. (2012). Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts. In International Symposium on Functional and Logic Programming (FLOPS).
  • Paul Downen and Zena M. Ariola. (2012). A Systematic Approach to Delimited Control with Multiple Prompts. In European Symposium on Programming (ESOP).