P.B.Levy. Broad Infinity and Generation Principles [Preprint], Notre Dame Journal of Formal Logic, volume 66(1), pages 79-141, 2025 © University of Notre Dame.
P.B.Levy. The Price of Mathematical Scepticism [Preprint], Philosophia Mathematica, volume 30(3), pages 283-305, 2022 © Oxford Academic.
P.B.Levy. Semantics Column: Call-By-Push-Value [Preprint], in ACM SIGLOG News 9(2) pages 7-29, 2022 © ACM. With an introduction by Mike Mislove.
B.Jacobs, P.B.Levy, J.Rot. Steps and Traces, Journal of Logic and Computation 31(6), pages 1482-1525, 2021 © Oxford Academic. Expanded version of Steps and Traces [Preprint] by the same authors, in the CMCS 2018 Proceedings, LNCS 11202, pages 122-143 © Springer.
P.B.Levy. Strong functors on many-sorted sets, Commentationes Mathematicae Universitatis Carolinae 60(4) (2019), special issue in memory of Věra Trnková.
P.B.Levy, S.Goncharov. Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot Proceedings, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO) 2019.
N.Bowler, P.B.Levy, G.D.Plotkin. Initial algebras and final coalgebras consisting of nondeterministic finite trace strategies 34th conference on the Mathematical Foundations of Programming Semantics, 2018. © Elsevier.
P.B.Levy. A ghost at ω1 Logical Methods in Computer Science 14(3), 2018, part of the Jiří Adámek festschrift.
M.Devesas Campos, P.B.Levy. A syntactic view of computational adequacy Proceedings of FoSSaCS 2018, LNCS 10803 © Springer.
U.Dal Lago, F.Gavazzo, P.B.Levy. Effectful Applicative Bisimilarity: Monads, Relators and Howe's Method [Preprint and long version] in Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 © IEEE.
O.Kammar, P.B.Levy, S.Moss, S.Staton. A monad for full ground reference cells [Preprint] Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 © IEEE.
P.B.Levy. Contextual isomorphisms [Preprint] in Proceedings of POPL 2017, pages 400-414 © ACM.
B.Geron, P.B.Levy. Iteration and labelled iteration Proceedings of MFPS 2016, ENTCS volume 325, pages 127-146 © Elsevier.
P.B.Levy. Final coalgebras from corecursive algebras [Preprint]in Proceedings of CALCO 2015.
J.Adámek, P.B.Levy, S.Milius, L.S.Moss, L.Sousa. On final coalgebras of power-set functors and saturated trees [Preprint], Applied Categorical Structures, volume 23, issue 4, pages 609-641, special issue dedicated to George Janelidze on the occasion of his sixtieth birthday, 2015, © Springer.
P.B.Levy, S.Staton. Transition systems over games [Preprint] in Proceedings, Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, Vienna, Austria, 2014 © ACM.
N.Bowler, S.Goncharov, P.B.Levy, L.Schröder. Exploring the boundaries of monad tensorability on Set in Logical Methods in Computer Science 9(3) paper 22, 2013.
S.Staton, P.B.Levy. Universal properties for impure programming languages [Preprint] in Proceedings, 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Rome, Italy, January 2013 © ACM.
R.Perera, U.A.Acar, J.Cheney, P.B.Levy. Functional programs that explain their work [Technical report] in Proceedings, 17th ACM SIGPLAN International Conference on Functional Programming, Copenhagen, Denmark, September 2012 © ACM.
J.Adámek, N.Bowler, P.B.Levy, S.Milius. Coproducts of monads on Set [Preprint with proofs] in Proceedings, 27th Annual ACM/IEEE Symposium on Logic in Computer Science, Dubrovnik, Croatia, June 2012, pages 45-54 © IEEE.
L.Aceto, A.Ingólfsdóttir, P.B.Levy, J.Sack. Characteristic formulae: a general approach [Preprint from 2010], Mathematical Structures in Computer Science 22(2), special issue devoted to papers from EXPRESS 2009, pages 125-173, © Cambridge University Press, 2012.
V.Koutavas, P.B.Levy, E.Summii. From applicative to environmental bisimulation [Preprint], Proceedings, 27th conference on the Mathematical Foundations of Programming Semantics, Carnegie Mellon, Pittsburgh, PA, May 2011, ENTCS volume 276, pages 215-235 (article 12) © Elsevier. Expanded version of Limitations of applicative bisimulation (preliminary report) by the same authors, Proceedings, Dagstuhl seminar on Modelling, controlling and reasoning about state, 2010.
P.B.Levy. Similarity Quotients as Final Coalgebras [Preprint]. In M.Hofmann (ed.), Proceedings, 14th international conference on Foundations of Software Science and Computation Structures, Saarbruecken, Germany, March-April 2011, LNCS vol. 6604, pages 27-41, © Springer. Here is a long version with proofs and additional results.
P.B.Levy. Characterizing recursive programs up to bisimilarity [Preprint], Proceedings of the 7th Workshop on Fixed Points in Computer Science, Brno, Czech Repulbic, August 2010, HAL-INRIA 00512377, pages 47-52.
T.Altenkirch, P.B.Levy and S.Staton. Higher-order containers [Preprint] in Programs, Proofs, Processes 6th Conference on Computability in Europe, Ponta Delgada (Azores), Portugal, July 2010, LNCS vol 6158, pages 11-20, © Springer.
P.B.Levy and K.Y.Weldemariam. Exploratory functions on nondeterministic strategies, up to lower bisimilarity [Preprint] Proceedings, 25th conference on the Mathematical Foundations of Programming Semantics, Oxford UK, April 2009, ENTCS volume 249, pages 357-375 (article 19) © Elsevier.
S.B.Lassen and P.B.Levy. Typed normal form bisimulation for parametric polymorphism [Preprint] Proceedings, 23rd Annual IEEE Syposium on Logic in Computer Science, Carnegie Mellon University, Pittsburgh PA USA, June 2008, pages 341-352 © IEEE.
P.B.Levy. Global state considered helpful [Preprint] Proceedings, 24th conference on the Mathematical Foundations of Programming Semantics, University of Pennsylvania, Philadelphia PA USA, May 2008, ENTCS volume 218, pages 241-259 (article 15) © Elsevier.
P.B.Levy. Infinite trace equivalence [Preprint] Annals of Pure and Applied Logic, vol. 151(2-3), pages 170-198, February 2008, special issue for for the 1st workshop on Games for Logic and Programming (GaLoP) 2005 © Elsevier. Expanded version of Infinite trace equivalence [Preprint] by the same author in Proceedings, 21st Conference on the Mathematical Foundations of Programming Semantics, Birmingham, U.K., June 2005, ENTCS volume 155 (published 2006), pages 467-496 (article 22) © Elsevier.
S.B.Lassen and P.B.Levy. Typed normal form bisimulation [Preprint]. LNCS vol. 4646, J. Duparc and T. A. Henzinger (eds.), Proceedings of the 6th EACSL Annual Conference on Computer Science and Logic (CSL 07), Lausanne, Switzerland, September 2007, pages 283-297 © Springer.
P.B.Levy. Amb breaks well-pointedness, ground amb doesn't [Preprint]. Proceedings of the 23rd conference on the Mathematical Foundations of Programming Semantics, New Orleans, April 2007, ENTCS volume 173, pages 221-239 (article 14) © Elsevier.
J.M.E.Hyland, P.B.Levy, G.D.Plotkin and A.J.Power. Combining algebraic effects with continuations [Preprint], Festschrift for John Reynolds' 70th birthday, Theoretical Computer Science, vol. 375 (1-3), pages 20-40, May 2007 © Elsevier. Expanded version of Combining continuations with other effects [Preprint] by the same authors, 4th ACM-SIGPLAN Continuation Workshop, Venice, Italy, January 2004.
P.B.Levy. Call-by-push-value: decomposing call-by-value and call-by-name [Preprint], Higher-Order and Symbolic Computation, volume 19(4), pages 377-414, December 2006 © Springer. Expanded version of Call-by-push-value: a subsuming paradigm (Extended Abstract) [Preprint] by the same author in Proceedings, 4th International Conference on Typed Lambda-Calculi and Applications, L'Aquila, Italy, LNCS volume 1581, pages 228-242, 1999 © Springer.
P.B.Levy. Jumbo lambda-calculus [Preprint] LNCS vol. 4052, M. Bugliesi, B. Preneel, V. Sassone, I. Wegener (eds.), Proceedings,33rd International Colloquium on Automata, Languages and Programming, Track B, Venice, Italy, July 2006, Part 2, pages 444-455 © Springer.
P.B.Levy. Monads and adjunctions for global exceptions [Preprint] Proceedings, 22nd Conference on the Mathematical Foundations of Programming Semantics, Genoa, Italy, 2006, ENTCS volume 158, pages 261-287 (article 14) © Elsevier.
P.B.Levy. Infinitary Howe's method [Preprint] Proceedings, 8th International Workshop on Coalgebraic Methods in Computer Science, Vienna, Austria, March 2006, ENTCS volume 164, issue 1, pages 85-104 (article 6) © Elsevier.
P.B.Levy. Jumping semantics for call-by-push-value [Preprint], O. Danvy and H. Thielecke eds., Proceedings, KAZAM Workshop, Birmingham, U.K., June 2005, University of Birmingham technical report CSR-06-10 (appeared 2006), pages 27-40.
P.B.Levy, A.J.Power and H.Thielecke. Modelling environments in call-by-value programming languages [Preprint] Information and Computation, 2003, vol. 185, pp. 182-210 © Elsevier.
P.B.Levy. Possible world semantics for general storage in call-by-value [Preprint] LNCS vol. 2471 , J. Bradfield ed., Proceedings, Computer Science Logic, Edinburgh, September 2002, pages 232-246 © Springer.
P.B.Levy. Adjunction models for call-by-push-value with stacks Theory and Applications of Categories, volume 14 (2005), article 5 (pages 75-110). Expanded version of Adjunction models for call-by-push-value with stacks [Preprint] by the same author in Proceedings, 9th Conference on Category Theory in Computer Science, Ottawa, August 2002, ENTCS volume 69, article 13, pages 248-271 © Elsevier.
P.B,Levy. Call-by-push-value. A functional/imperative synthesis, Semantic Structures in Computation, © Springer, 2004.
P.B.Levy. Call-by-push-value PhD thesis, Queen Mary, University of London, 2001.
N.Krishnaswami, P.B.Levy, eds. Proceedings of the 5th workshop on Mathematically Structured Functional Programming, Grenoble, France, April 2014. Volume 153 of EPTCS.
J.M.Chapman, P.B.Levy, eds. Proceedings of the 4th workshop on Mathematically Structured Functional Programming, Tallinn, Estonia, March 2012. Volume 76 of EPTCS.
S.B.Lassen, P.B.Levy, P.Panangaden. Divergence-least semantics of amb is Hoare [pdf]. Short presentation at the 3rd APPSEM II workshop, September 2005, Frauenchiemsee, Germany.
P.B.Levy. Martin-Löf clashes with Griffin, operationally [pdf]
S.B.Lassen and P.B.Levy. Some parametricity isomorphisms [pdf]
P.B.Levy. Modal properties of recursively defined commands (work in progress) [pdf] to be presented at Domains IX
P.B.Levy. Boolean precongruences [ pdf ]
The price of mathematical scepticism [pdf]
Locally graded categories [pdf]
Adjunction semantics for call-by-push-value [pdf]
Amb breaks well-pointedness, ground amb doesn't [pdf]
Nondeterminism, fixpoints and bisimulation [pdf]
Semantics of nondeterminism [pdf] a talk intended for a general computer science audience
A tutorial on call-by-push-value [pdf] given at the Workshop on Effects and Type Theory
Normal form bisimulation for polymorphism [pdf]
Modal properties of recursive programs work in progress [pdf]
Pointer game semantics for polymorphism (work in progress - presented at GALOP 2010) [pdf]
Morphisms between plays [pdf]