Call-by-Push-Value: A Subsuming Paradigm. - Paul Blain Levy (TLCA, 1999)

Call-by-push-value. - Paul Blain Levy (2001)

Possible World Semantics for General Storage in Call-By-Value. - Paul Blain Levy (CSL, 2002)

Adjunction Models For Call-By-Push-Value With Stacks. - Paul Blain Levy (CTCS, 2002)

Modelling environments in call-by-value programming languages. - Paul Blain Levy; John Power; Hayo Thielecke (Inf. Comput., 2003)

Call-By-Push-Value: A Functional/Imperative Synthesis - Paul Blain Levy (Springer, 2004)

Infinite Trace Equivalence. - Paul Blain Levy (MFPS, 2005)

Jumbo lambda-Calculus. - Paul Blain Levy (ICALP (2), 2006)

Monads and Adjunctions for Global Exceptions. - Paul Blain Levy (MFPS, 2006)

Infinitary Howe's Method. - Paul Blain Levy (CMCS, 2006)

Call-by-push-value: Decomposing call-by-value and call-by-name. - Paul Blain Levy (High. Order Symb. Comput., 2006)

Typed Normal Form Bisimulation. - Søren B. Lassen; Paul Blain Levy (CSL, 2007)

Amb Breaks Well-Pointedness, Ground Amb Doesn't. - Paul Blain Levy (MFPS, 2007)

Combining algebraic effects with continuations. - Martin Hyland; Paul Blain Levy; Gordon D. Plotkin; John Power (Theor. Comput. Sci., 2007)

Typed Normal Form Bisimulation for Parametric Polymorphism. - Søren B. Lassen; Paul Blain Levy (LICS, 2008)

Global State Considered Helpful. - Paul Blain Levy (MFPS, 2008)

Exploratory Functions on Nondeterministic Strategies, up to Lower Bisimilarity. - Paul Blain Levy; Kidane Yemane Weldemariam (MFPS, 2009)

Higher-Order Containers. - Thorsten Altenkirch; Paul Blain Levy; Sam Staton (CiE, 2010)

Limitations of Applicative Bisimulation (Preliminary Report). - Vasileios Koutavas; Paul Blain Levy; Eijiro Sumii (Modelling, Controlling and Reasoning About State, 2010)

Characterizing Recursive Programs up to Bisimilarity. - Paul Blain Levy (FICS, 2010)

Similarity Quotients as Final Coalgebras. - Paul Blain Levy (FoSSaCS, 2011)

From Applicative to Environmental Bisimulation. - Vasileios Koutavas; Paul Blain Levy; Eijiro Sumii (MFPS, 2011)

Functional programs that explain their work. - Roly Perera; Umut A. Acar; James Cheney; Paul Blain Levy (ICFP, 2012)

Coproducts of Monads on Set. - Jirí Adámek; Stefan Milius; Nathan J. Bowler; Paul Blain Levy (LICS, 2012)

Characteristic formulae for fixed-point semantics: a general framework. - Luca Aceto; Anna Ingólfsdóttir; Paul Blain Levy; Joshua Sack (Math. Struct. Comput. Sci., 2012)

Universal properties of impure programming languages. - Sam Staton; Paul Blain Levy (POPL, 2013)

Exploring the Boundaries of Monad Tensorability on Set. - Nathan J. Bowler; Sergey Goncharov 001; Paul Blain Levy; Lutz Schröder (Log. Methods Comput. Sci., 2013)

Transition systems over games. - Paul Blain Levy; Sam Staton (CSL-LICS, 2014)

Final Coalgebras from Corecursive Algebras. - Paul Blain Levy (CALCO, 2015)

On Final Coalgebras of Power-Set Functors and Saturated Trees - To George Janelidze on the Occasion of His Sixtieth Birthday. - Jirí Adámek; Paul Blain Levy; Stefan Milius; Lawrence S. Moss; Lurdes Sousa (Appl. Categorical Struct., 2015)

A Ghost at $ω_1$. - Paul Blain Levy (CoRR, 2016)

Iteration and Labelled Iteration. - Bram Geron; Paul Blain Levy (MFPS, 2016)

A monad for full ground reference cells. - Ohad Kammar; Paul Blain Levy; Sean K. Moss; Sam Staton (LICS, 2017)

Effectful applicative bisimilarity: Monads, relators, and Howe's method. - Ugo Dal Lago; Francesco Gavazzo; Paul Blain Levy (LICS, 2017)

Contextual isomorphisms. - Paul Blain Levy (POPL, 2017)

Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method (Long Version). - Ugo Dal Lago; Francesco Gavazzo; Paul Blain Levy (CoRR, 2017)

A Syntactic View of Computational Adequacy. - Marco Devesas Campos; Paul Blain Levy (FoSSaCS, 2018)

Initial Algebras and Final Coalgebras Consisting of Nondeterministic Finite Trace Strategies. - Nathan J. Bowler; Paul Blain Levy; Gordon D. Plotkin (MFPS, 2018)

A Ghost at ω1. - Paul Blain Levy (Log. Methods Comput. Sci., 2018)

Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot. - Paul Blain Levy; Sergey Goncharov 001 (CALCO, 2019)

Steps and traces. - Jurriaan Rot; Bart Jacobs 001; Paul Blain Levy (J. Log. Comput., 2021)

Call-by-push-value. - Paul Blain Levy (ACM SIGLOG News, 2022)

Probabilistic Strategies: Definability and the Tensor Completeness Problem. - Nathan J. Bowler; Sergey Goncharov 001; Paul Blain Levy (CoRR, 2025)

What is a monoid? - Paul Blain Levy; Morgan Rogers (CoRR, 2025)