8 citations · 11 across the 9 of their papers we have counts for
9 papers
Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory (Extended Version)
Eric Giovannini, Tingting Ding, Max S. New
Gradually typed programming languages, which allow for soundly mixing static and dynamically typed programming styles, present a strong challenge for metatheorists. Even the simple…
Gradual Typing for Effect Handlers
Max S. New, Eric Giovannini, Daniel R. Licata
We present a gradually typed language, GrEff, with effects and handlers that supports migration from unchecked to checked effect typing. This serves as a simple model of the integr…
A Formal Logic for Formal Category Theory (Extended Version)
Max S. New, Daniel R. Licata
We present a domain-specific type theory for constructions and proofs in category theory. The type theory axiomatizes notions of category, functor, profunctor and a generalized for…
Proceedings Ninth Workshop on Mathematically Structured Functional Programming
Jeremy Gibbons, Max S. New
This volume contains the proceedings of the Ninth Workshop on Mathematically Structured Functional Programming (MSFP 2022). The meeting took place on the 2nd of April as a satellit…
Proceedings Eighth Workshop on Mathematically Structured Functional Programming
Max S. New, Sam Lindley
This volume contains the proceedings of the Eighth Workshop on Mathematically Structured Functional Programming (MSFP 2020). The meeting was originally scheduled to take place in D…
Gradual Type Theory (Extended Version)
Max S. New, Daniel R. Licata, Amal Ahmed
Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type…
Graduality from Embedding-projection Pairs (Extended Version)
Max S. New, Amal Ahmed
Gradually typed languages allow statically typed and dynamically typed code to interact while maintaining benefits of both styles. The key to reasoning about these mixed programs i…
Call-by-name Gradual Type Theory
Max S. New, Daniel R. Licata
We present gradual type theory, a logic and type theory for call-by-name gradual typing. We define the central constructions of gradual typing (the dynamic type, type casts and typ…
FabULous Interoperability for ML and a Linear Language
Gabriel Scherer, Max New, Nick Rioux +1
Instead of a monolithic programming language trying to cover all features of interest, some programming systems are designed by combining together simpler languages that cooperate…