Paul Downen

I am an Assistant Professor in the Miner School of Computer & Information Sciences at University of Massachusetts, Lowell since Fall 2021.

Previously, I completed my Ph.D. from the University of Oregon's Department of Computer and Information Science.

My general research interests are in the study of programming languages, including their theory, semantics, design, and implementation, with a focus on the foundations of computation and its relation to logic and duality. In particular, I am interested in using logic to help verify that software systems and their compilation is efficient, correct, safe, and secure. I'm also interested in aspects of practical languages including computational effects (like mutable state, exceptions, and first-class continuations) and ways for languages to sensibly bridge between high-level abstractions and low-level implementation details.

I have worked on an alternative model for computation based on the connection between programming languages and formal logic (known as the Curry-Howard correspondence or proofs-as-programs interpretation). With a single stroke in 1935, Gentzen laid out the basis for the modern study of formalized logic: natural deduction and the sequent calculus. On the one hand, natural deduction is the logic of the lambda calculus, which serves as the bedrock for functional programming languages (like Scheme, Haskell, and OCaml) and proof assistants (like Coq). On the other hand, the sequent calculus has only recently been connected with a lower-level model for programs that highlights the dualities present in programming languages and details such as evaluation strategies (like strict or lazy evaluation) and control-flow effects (like exceptions). I am developing this model of computation to get another view of programs and languages from different angles:

• A high-level calculus for reasoning about the behavior of programs (in a similar style as the lambda calculus) while also accounting for low-level details such as evaluation strategy and control flow.
• A contextual representation of programs that allows for performing context-sensitive analysis and transformation of programs, as done by optimizing compilers like the Glasgow Haskell Compiler (GHC).
• A dualized framework that gives a symmetric and unified view of programming concepts, as a way to understand differences and similarities in language design, including types and abstraction mechanisms from both functional and object-oriented languages.

Some of these ideas have been (or are currently being) implemented inside GHC for analyzing and optimizing Haskell programs.

• Sequent Core (based on "Sequent Calculus as a Compiler Intermediate Language") is a plugin for GHC that replaces its Core intermediate language with an alternative one based on the sequent calculus.
• Join points (based on "Compiling Without Continuations") are an extension to the GHC Core language with purely functional labels and jumps, used to optimize branching control flow in programs.
• Static calling conventions (based on "Kinds Are Calling Conventions") are a type-based approach to integrating parametric polymorphism with C-like function calls, including number of arguments and their machine representations, completely at compile-time.

• Fall 2024: COMP.2030 Assembly Language Programming.
• Spring 2024: COMP.2030 Assembly Language Programming.
• Fall 2023: COMP.4600/5300 Effective Functional Programming.
• Fall 2023: COMP.2030 Assembly Language Programming.
• Spring 2023: COMP.3010 Organization of Programming Languages.
• Fall 2022: COMP.4600/5300 Effective Functional Programming.
• Summer 2022: COMP.3010 Organization of Programming Languages.
• Spring 2022: COMP.3010 Organization of Programming Languages.
• Fall 2021: COMP.5300 Effective Functional Programming.

• Foundations of Programming Languages, an intensive introduction to the fundamentals of the theory of programming languages, for graduate students, advanced undergraduate students, and interested experts from other fields. This course was given at the Oregon Programming Languages Summer School 2017 and 2018.


• Advanced Functional Programming, an application of advanced topics and techniques of functional programming for writing practical, interactive, and correct software. This course was given in Spring 2018.

• Lecture notes
• Accompanying Python template

Journal Articles

• Paul Downen and Zena M. Ariola. (2023). Classical (Co)Recursion: Mechanics. Journal of Functional Programming, Volume 33, e4.
  (doi)


• Paul Downen and Zena M. Ariola. (2020). Compiling With Classical Connectives. Logical Methods in Computer Science, Volume 16, Issue 3, pp. 13:1-13:57.
  (pdf) (online) (arXiv)


• Paul Downen, Zena M. Ariola, and Silvia Ghilezan. (2019). The duality of classical intersection and union types. Fundamenta Informaticae, 170, 2019.
  (pdf)


• 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, 2019.
  (pdf)


• Paul Downen and Zena M. Ariola. (2018). A Tutorial on Computational Classical Logic and the Sequent Calculus. Journal of Functional Programming, 28, e3.
  (doi) (pdf+appendix)


• Philip Johnson-Freyd, Paul Downen, and Zena M. Ariola. (2017). Call-by-Name Extensionality and Confluence. Journal of Functional Programming, 27, e12.
  (doi) (pdf+appendix)


• Philip Johnson-Freyd, Paul Downen, and Zena M. Ariola. (2016). First class call stacks: Exploring head reduction. In Olivier Danvy and Ugo de'Liguoro: Proceedings of the Workshop on Continuations, London, UK, (WoC2015), Electronic Proceedings in Theoretical Computer Science, 212, pp. 18–35.
  (arXiv) (pdf)


• Paul Downen and Zena M. Ariola. (2014). Delimited control and computational effects. Journal of Functional Programming, 24, pp 1-55.
  (doi) (pdf+appendix)

Conference and Workshop Papers

• Paul Downen. (2024). Call-By-Unboxed-Value. In International Conference on Functional Programming (ICFP2024).
  (pdf) (doi)


• Zachary J. Sullivan, Paul Downen, and Zena M. Ariola. (2023). Closure Conversion in Little Pieces. In Principles and Practice of Declarative Programming (PPDP2023).
  (pdf) (doi)


• Klaus Ostermann, David Binder, Ingo Skupin, Tim Süberkrüb, and Paul Downen. (2022). Introduction and elimination, left and right. In International Conference on Functional Programming (ICFP2022).
  (doi)


• Zachary J. Sullivan, Paul Downen, and Zena M. Ariola. (2021). Strictly Capturing Non-strict Closures. In Partial Evaluation and Program Manipulation (PEPM2021).
  (doi)


• Paul Downen and Zena M. Ariola. (2021). Duality In Action. In Formal Structures for Computation and Deduction (FSCD2021).
  (doi) (pdf)


• Paul Downen and Zena M. Ariola. (2020). A Computational Understanding of Classical (Co)Recursion. In Principles and Practice of Declarative Programming (PPDP2020).
  (doi) (pdf)


• Paul Downen, Zena M. Ariola, Simon Peyton Jones, and Richard A. Eisenberg. (2020). Kinds Are Calling Conventions. In International Conference on Functional Programming (ICFP2020).
  (doi) (pdf)


• Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. (2019). Making a Faster Curry with Extensional Types. In Haskell Symposium, Berlin, Germany (Haskell2019).
  (pdf)


• Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. (2019). Codata in action. In European Symposium on Programming, Prague, Czech Republic (ESOP2019).
  (pdf)


• Paul Downen and Zena M. Ariola. (2018). Beyond Polarity: Towards A Multi-Discipline Intermediate Language with Sharing. In Computer Science Logic, Birmingham, UK (CSL2018).
  (doi) (pdf) (pdf+appendix)


• Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola. (2018). Uniform Strong Normalization for Multi-Discipline Calculi. In International Workshop on Rewriting Logic and its Applications, Thessaloniki, Greece (WRLA2018).
  (pdf+appendix)


• Luke Maurer, Paul Downen, Zena M. Ariola, and Simon Peyton Jones. (2017). Compiling without Continuations. In Programming Language Design and Implementation, Barcelona, Spain (PLDI2017). Best Paper Award.
  (acm) (doi) (pdf) (pdf+appendix)


• Paul Downen, Luke Maurer, Zena Ariola, and Simon Peyton Jones. (2016). Sequent calculus as a compiler intermediate language. International Conference on Functional Programming, Nara, Japan (ICFP2016).
  (acm) (doi) (pdf) (appendix) (pdf+appendix)


• Luke Maurer, Paul Downen, Zena Ariola, and Simon Peyton Jones. (2016). Administrative normal form, continued. Higher-Order Programming with Effects, Nara, Japan (HOPE2016).
  (pdf)


• Paul Downen, Philip Johnson-Freyd, and Zena M. Ariola. (2015). Structures for structural recursion. International Conference on Functional Programming, Vancouver, BC, Canada (ICFP2015).
  (acm) (doi) (pdf) (extended)


• Philip Johnson-Freyd, Paul Downen, and Zena M. Ariola. (2015). Control controls extensional execution. Higher-Order Programming with Effects, Vancouver, BC, Canada (HOPE2015).
  (pdf)


• Paul Downen and Zena M. Ariola. (2014). Compositional semantics for composable continuations: from abortive to delimited control. International Conference on Functional Programming, Gothenburg, Sweden (ICFP2014).
  (acm) (doi) (pdf)


• Paul Downen and Zena M. Ariola. (2014). Delimited control with multiple prompts in theory and practice. Higher-Order Programming with Effects, Gothenburg, Sweden (HOPE2014).
  (pdf)


• Paul Downen, Luke Maurer, Zena M. Ariola, and Daniele Varacca. (2014). Continuations, processes, and sharing. Principles and Practice of Declarative Programming, Canterbury, UK (PPDP2014).
  (acm) (doi) (pdf)


• Paul Downen and Zena M. Ariola. (2014). The duality of construction. European Symposium on Programming, Grenoble, France (ESOP2014).
  (doi) (pdf)


• Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, and Alexis Saurin. (2012). Classical call-by-need sequent calculi: The unity of semantic artifacts. International Symposium on Functional and Logic Programming, Kobe, Japan (FLOPS2012).
  (doi) (pdf)


• Paul Downen and Zena M. Ariola. (2012). A Systematic Approach to Delimited Control with Multiple Prompts. European Symposium on Programming, Tallinn, Estonia (ESOP2012). Best Paper Award nominee.
  (doi) (pdf)

Unpublished Manuscripts

• Paul Downen. (2017). Sequent Calculus: A Logic and a Language for Computation and Duality. Ph.D. thesis, University of Oregon.
  (pdf)


• Paul Downen. (2014). Computational Duality and the Sequent Calculus. Comprehensive Area Exam Report, University of Oregon.
  (pdf)


• Paul Downen and Zena M. Ariola. (2021). Classical (Co)Recursion: Programming.
  (arXiv)


• Paul Downen and Zena M. Ariola. (2017). A Polar Basis for Simple Types.
  (pdf)


• Paul Downen. (2024). Foundations of Programming Languages. Lecture notes for course at the Oregon Programming Languages Summer School, June 3-8, 2024.
  (pdf)


• Paul Downen. (2022). Abstract Machines and Classical Realizability. Lecture notes for course at the Oregon Programming Languages Summer School, June 24-27, 2022.
  (pdf)


• Paul Downen. (2014). Bi-orthogonality. Personal notes on bi-orthogonal models of type systems, originally written in August, 2014.
  (pdf)

Conference Talks

• Call-By-Unboxed-Value.
  Venue: International Conference on Functional Programming. September 3, 2024.
  Slides: (pdf)


• Kinds are Calling Conventions.
  Venue: Programming Language Design and Implementation. June 16, 2022.
  Slides: (pdf)


• A Computational Understanding of (Co)Recursion.
  Venue: Principles and Practice of Declarative Programming. September 10, 2020.
  Slides: (pdf)
  Video (mp4)


• Kinds are Calling Conventions.
  Venue: International Conference on Functional Programming. August 27, 2020.
  Slides: (pdf)
  Video (mp4)


• Codata in action.
  Venue: European Symposium on Programming, Prague, Czech Republic. April 8, 2019.
  Slides: (pdf)


• Beyond Polarity: Towards A Multi-Discipline Intermediate Language with Sharing.
  Venue: Computer Science Logic, Birmingham, UK. September 4, 2019.
  Slides: (pdf)


• Sequent calculus as a compiler intermediate language.
  Venue: International Conference on Functional Programming, Nara, Japan. September 19, 2016.
  Slides: (pdf)
  Video: (youtube)


• Structures for structural recursion.
  Venue: International Conference on Functional Programming, Vancouver, BC, Canada. August 31, 2015.
  Slides: (pdf)
  Video: (youtube)


• Continuations, processes, and sharing.
  Venue: Principles and Practice of Declarative Programming, Canterbury, UK. September 8, 2014.
  Slides: (pdf)


• Compositional Semantics for Composable Continuations: From Abortive to Delimited Control.
  Venue: International Conference on Functional Programming, Gothenburg, Sweden. September 1, 2014.
  Slides: (pdf)
  Video: (youtube)


• The duality of construction.
  Venue: European Symposium on Programming, Grenoble, France. April 9, 2014.
  Slides: (pdf)


• A Systematic Approach to Delimited Control with Multiple Prompts.
  Venue: European Symposium on Programming, Tallinn, Estonia. March 26, 2012.
  Slides: (pdf)

Workshop Talks

• Control controls extensional execution.
  Venue: Higher-Order Programming with Effects, Vancouver, BC, Canada. August 30, 2015.
  Slides: (pdf)


• Delimited control with multiple prompts in theory and practice.
  Venue: Higher-Order Programming with Effects, Gothenburg, Sweden. August 31, 2014.
  Slides: (pdf)
  Video: (youtube)

Invited Talks

• Logic In Action.
  Venue: University of Massachusetts, Lowell, MA. April 15, 2021.
  Venue: University of Vermont, Burlington, VT. March 17, 2021.
  Slides: (pdf)


• Kinds Are Calling Convnetions: Intensional Static Polymorphism.
  Venue: Principles of Programming and Verification, Boston University, Boston, MA. November 17, 2020.
  Slides: (pdf)


• Beyond Polarity: Towards A Multi-Discipline Intermediate Language with Sharing.
  Venue: University of Cambridge, UK. September 11, 2019.
  Venue: Microsoft Research, Cambridge, UK. September 10, 2019.
  Slides: (pdf)


• The structures of induction and co-induction.
  Venue: Microsoft Research Lecture, Cambridge, UK. September 17, 2015.


• The duality of construction.
  Venue: McGill University, Montreal, QC, Canada. November 6, 2014.


• Building up delimited control with multiple prompts.
  Venue: INRIA Preuves, Programmes et Systèmes, Théorie des types et réalisabilité, Paris, France. December 19, 2012.


• Opening the Black Box: Profiling Computer Memory.
  Venue: Lawrence Technological University, Arts and Science Seminar Series, Southfield, MI, USA. February 11, 2010.