P.B.Levy. Semantics Column: Call-By-Push-Value [Preprint], in ACM SIGLOG News 9(2) pages 7-29, 2022. 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. This is an expanded version of the paper [Preprint] in CMCS 2018, which appeared in LNCS 11202 © Springer.
P.B.Levy. Strong functors on many-sorted sets [Preprint] 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] Proceedings of LICS 2017.
O.Kammar, P.B.Levy, S.Moss, S.Staton. A monad for full ground reference cells [Preprint] Proceedings of LICS 2017.
P.B.Levy. Contextual isomorphisms [Preprint] Proceedings of POPL 2017.
B.Geron, P.B.Levy. Iteration and labelled iteration Proceedings of MFPS 2016.
P.B.Levy. Final coalgebras from corecursive algebras Proceedings of CALCO 2015 [Preprint]
J.Adámek, P.B.Levy, S.Milius, L.S.Moss, L.Sousa. On final coalgebras of power-set functors and saturated trees Applied Categorical Structures, volume 23, issue 4, pages 609-641, special issue dedicated to George Janelidze on the occasion of his sixtieth birthday, 2015, [preprint] © Springer
P.B.Levy, S.Staton. Transition systems over games,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 [Preprint] © 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, in Proceedings, Fortieth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Rome, Italy, January 2013 © ACM [Preprint]
R.Perera, U.A.Acar, J.Cheney, P.B.Levy. Functional programs that explain their work in Proceedings 17th ACM-SIGPLAN International Conference on Functional Programming, Copenhagen, Denmark, September 2012 © ACM [Preprint] (Supplementary technical report)
J.Adámek, N.Bowler, P.B.Levy, S.Milius. Coproducts of monads on Set in Proceedings, 27th Annual ACM/IEEE Symposium on Logic in Computer Science, Dubrovnik, Croatia, June 2012, pages 45-54 © IEEE Press. Here is an extended version with proofs.
L.Aceto, A.Ingólfsdóttir, P.B.Levy, J.Sack. Characteristic formulae: a general approach. Preprint version dated 18 August 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. (An early version may be found here.)
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 [Preprint] 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.
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 GaLoP 2005 © 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.
P.B.Levy. Call-by-push-value: decomposing call-by-value and call-by-name [Preprint], Higher-Order and Symbolic Computation, vol. 19(4), pages 377-414, December 2006 © 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, May 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. Infinite trace equivalence [Preprint] 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.
J.M.E.Hyland, P.B.Levy, G.D.Plotkin and A.J.Power. Combining continuations with other effects [Preprint] 4th ACM-SIGPLAN Continuation Workshop, Venice, Italy, January 2004.
P.B.Levy, A.J.Power and H.Thielecke. Modelling environments in call-by-value programming languages [Preprint] © Elsevier, Information and Computation, 2003, vol. 185, pp. 182-210.
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).
P.B.Levy. Adjunction models for call-by-push-value with stacks [Preprint] Proceedings, Category Theory in Computer Science 2002, Ottawa, August 2002, ENTCS vol. 69, article 13 © 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.
P.B.Levy. Call-By-Push-Value: A Subsuming Paradigm (Extended Abstract) [Preprint] LNCS vol. 1581, J.-Y. Girard, ed., Proceedings, Typed Lambda-Calculi and Applications, L'Aquila, Italy, April 1999, pages 228-242 © Springer.
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.
P.B.Levy Thunkable implies central [pdf]
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]