Manuscripts

• A Semantic Foundation for Sound Gradual Typing
  Max S. New
  PhD Thesis, Northeastern University, 2020
  dissertation

Peer-Reviewed Papers

• Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory
  Eric Giovannini, Tingting Ding and Max S. New
  POPL 2025
  extended version

• Gradual Typing for Effect Handlers
  Max S. New and Eric Giovannini and Daniel R. Licata
  OOPSLA 2023
  Extended Version

• A formal type theory for formal category theory
  Max S. New and Daniel R. Licata
  FoSSaCS 2023
  official-link repo

• Gradual Type Theory
  Max S. New and Daniel R. Licata and Amal Ahmed
  JFP Vol 31, 2021
  doi

• Call-by-name Gradual Type Theory
  Max S. New, Daniel R. Licata
  Logical Methods in Computer Science, Volume 16, Issue 1
  Arxiv backup LMCS Link
  subsumes earlier conference paper of the same name published at FSCD

• Graduality and Parametricity: Together Again for the First Time
  Max S. New, Dustin Jamner, Amal Ahmed
  POPL 2020
  Official Link Preprint Technical Appendix

• How to evaluate the performance of gradual type systems
  Ben Greenman, Asumu Takikawa, Max S. New, Daniel Feltey, Robert Bruce Findler, Jan Vitek, Matthias Felleisen
  Journal of Functional Programming, Volume 29, 2019
  Official Link Preprint

• Gradual Type Theory
  Max S. New, Daniel R. Licata, Amal Ahmed
  POPL 2019
  Extended Version Official Link

• Graduality from Embedding-Projection Pairs
  Max S. New, Amal Ahmed
  ICFP 2018
  Conference Talk Extended Version Official Link

• Call-by-name Gradual Type Theory
  Max S. New, Daniel R. Licata
  FSCD 2018
  Official Link
  subsumed by journal article of the same name published in LMCS

• FabULous Interoperability for ML and a Linear Language
  Gabriel Scherer, Max S. New, Nick Rioux and Amal Ahmed
  FoSSaCS 2018
  Preprint Supplementary material

• Fair enumeration combinators
  Max S. New, Burke Fetscher, Robert Bruce Findler, Jay McCarthy
  Journal of Functional Programming, Volume 27, 2017
  Official Link

• Fully Abstract Compilation via Universal Embedding
  Max S. New, William J. Bowman, Amal Ahmed
  ICFP 2016
  Conference talk Extended Technical Report Official Link Preprint

• Oh Lord, Please Don't Let Contracts be Misunderstood (Functional Pearl)
  Christos Dimoulas, Max S. New, Robert Bruce Findler, Matthias Felleisen
  ICFP 2016
  Official Link

• A Coq Library For Internal Verification of Running-Times
  Jay McCarthy, Burke Fetscher, Max New, Daniel Feltey, Robert Bruce Findler
  FLOPS 2016
  Repository

• Is Sound Gradual Typing Dead?
  Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, Matthias Felleisen
  POPL 2016
  Official Link

Drafts

• Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus
  Steven Schaefer, Nathan Varner, Pedro H. Azevedo de Amorim and Max S. New
  draft

• Notions of Stack-manipulating Computation and Relative Monads
  Yuchen Jiang, Runze Xue and Max S. New
  draft

Talks and Abstracts

• Compiling with Call-by-push-value
  Max S. New
  Invited talk, MFPS 2023
  slides

• Relative Monads in Call-by-push-value as an Abstraction of Stack-Based Effects
  Max S. New
  HOPE 2022
  Extended Abstract Talk slides

• From Call-by-push-value to Stack-based TAL?
  Max S. New
  LOLA 2019
  Extended Abstract

• Gradual Type Precision as Retraction
  Max S. New
  POPL 2017 Student Research Competition
  Extended Abstract Poster